class Datum

functions

private static

gueltigesDatum : ℕ_{1} × ℕ_{1} × ℕ_{1} → 𝔹 gueltigesDatum (t, m, j ) \underline{△}

1920 ≤ j ∧

j ≤ 2100 ∧

m ≤ 12 ∧

t ≤

cases m :

4, 6, 9, 11 → 30,

2 → if ((j rem 4 = 0) ∧ ¬ (j rem 100 = 0)) ∨

(j rem 400 = 0) then 29 else 28, others → 31

end

instance variables

Tag : ℕ_{1};

Monat : ℕ_{1};

Jahr : ℕ_{1};

inv gueltigesDatum (Tag, Monat, Jahr)

values

public static

invalidDatum = Datum (31, 12, 2100)

operations

Datum : ℕ_{1} × ℕ_{1} × ℕ_{1} →^{o} Datum Datum (t, m, j ) \underline{△}

( Tag := t; Monat := m; Jahr := j

) pre gueltigesDatum (t, m, j ) ;

public static

today : () →^{o} Datum today () \underline{△}

is not yet specified;

public

minus : Datum →^{o} ℕ minus (d) \underline{△}

if Monat > d.Monat

then return Jahr − d.Jahr elseif Monat < d.Monat then return Jahr − d.Jahr − 1 elseif Tag ≥ d.Tag then return Jahr − d.Jahr else return Jahr − d.Jahr − 1

pre d.groesserGleich (self) ;

public

groesserGleich : Datum →^{o} 𝔹 groesserGleich (d) \underline{△}

if Jahr > d.Jahr

then return true

elseif Jahr < d.Jahr

then return false

elseif Monat > d.Monat

then return true

elseif Monat < d.Monat

then return false

elseif Tag ≥ d.Tag

then return true
else return false

pre true ;

public

inbetween : Datum × Datum →^{o} 𝔹 inbetween (von, bis) \underline{△}

return bis.groesserGleich (self) ∧ self.groesserGleich (von) end Datum