|
\section{The Class Clock}
This class models a clock which maintains a date.
\begin{vdm_al}
class Clock
types
public Date = seq of char;
instance variables
date : Date := [];
operations
public SetDate : Date ==> ()
SetDate(d) ==
date := d;
pure public GetDate : () ==> Date
GetDate() ==
return date;
end Clock
\end{vdm_al}
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
