{\small\sf class} $Datum$
\par
\kFunctions
\kw{\kw{private}\kw{ }\kw{static}}\begin{fn}[e]{gueltigesDatum}%
\signature{\Natone  \X \Natone  \X \Natone  \To \Bool }
\parms*{\Lp t,m,j\Rp }
\annlab[o]{Datum`gueltigesDatum}
1920 \Le j \And  \\
j \Le 2100 \And  \\
m \Le 12 \And  \\
t \Le  \\
\begin{Cases}{m}
\alt{4,6,9,11}{30}
\alt{2}{\If \pex{\pex{j \Rem 4 = 0} \And  \Not \pex{j \Rem 100 = 0}} \Or  \\
\pex{j \Rem 400 = 0}
\Then \\
29
\Else \\
28
\Fi}
\others{31}
\end{Cases}
\end{fn}
\kInstanceVarDef
\parlinebr
\begin{insvar}
\assdef{Tag}{\Natone }
\end{insvar}
\begin{insvar}
\assdef{Monat}{\Natone }
\end{insvar}
\begin{insvar}
\assdef{Jahr}{\Natone }
\end{insvar}
\begin{instinvfn}
\fnapply{gueltigesDatum}{Tag,Monat,Jahr}\end{instinvfn}
\par
\kValues
\kw{\kw{public}\kw{ }\kw{static}}\val{invalidDatum}{\fnapply{Datum}{31,12,2100}}
\kOperations
\kw{}\begin{op}[e]{Datum}%
\signature{\Natone  \X \Natone  \X \Natone  \Oto Datum}
\parms{t,m,j}
\annlab[o]{Datum`Datum}
\begin{blockstmt}
\ass{Tag}{t} ; \\
\ass{Monat}{m} ; \\
\ass{Jahr}{j}
\end{blockstmt}
\begin{precond}
\fnapply{gueltigesDatum}{t,m,j}
\end{precond};
\end{op}
\kw{\kw{public}\kw{ }\kw{static}}\begin{op}[e]{today}%
\signature{() \Oto Datum}
\parms{}
\annlab[o]{Datum`today}
\isnotyetspec;
\end{op}
\kw{\kw{public}}\begin{op}[e]{minus}%
\signature{Datum \Oto \Nat }
\parms{d}
\annlab[o]{Datum`minus}
\If Monat > d.Monat
\Then \\
\return{Jahr \Minus d.Jahr}
\Elseif Monat < d.Monat
\Then \\
\return{Jahr \Minus d.Jahr \Minus 1}
\Elseif Tag \Ge d.Tag
\Then \\
\return{Jahr \Minus d.Jahr}
\Else \\
\return{Jahr \Minus d.Jahr \Minus 1}
\Fi
\begin{precond}
\fnapply{d.groesserGleich}{\kSelf }
\end{precond};
\end{op}
\kw{\kw{public}}\begin{op}[e]{groesserGleich}%
\signature{Datum \Oto \Bool }
\parms{d}
\annlab[o]{Datum`groesserGleich}
\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 \Ge d.Tag
\Then \\
\return{\True }
\Else \\
\return{\False }
\Fi
\begin{precond}
\True 
\end{precond};
\end{op}
\kw{\kw{public}}\begin{op}[e]{inbetween}%
\signature{Datum \X Datum \Oto \Bool }
\parms{von,bis}
\annlab[o]{Datum`inbetween}
\return{\fnapply{bis.groesserGleich}{\kSelf } \And \fnapply{\kSelf .groesserGleich}{von}}
\end{op}
{\small\sf end} {\it Datum}

