| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMPP/CashDispenserConcPP/ (Wiener Entwicklungsmethode ©) Datei vom 13.4.2020 mit Größe 1 kB |
|
SSL Timer.vdmpp
Interaktion und |
|||||||||
|
\section{The Timer Class}
The Timer class is a straightforward periodic timer which increments its clock in its own thread. It provides operations for starting, and stopping timing, and reading the current time. \begin{vdm_al} class Timer \end{vdm_al} The Timer has two instance variables the current time and a flag indicating whether the Timer is active or not (the current time is only incremented if the Timer is active). \begin{vdm_al} instance variables curTime : nat := 0; active : bool := false; \end{vdm_al} The Timer provides straightforward operations which need no further explanation. \begin{vdm_al} operations public Start : () ==> () Start() == (active := true; curTime := 0); public Stop : () ==> () Stop() == active := false; pure public GetTime : () ==> nat GetTime() == return curTime; IncTime: () ==> () IncTime() == if active then curTime := curTime + 100; \end{vdm_al} The Timer's thread ensures that the current time is incremented. We take one time unit for our Timer to correspond to 10 system time units. \begin{vdm_al} -- FIXME: Example used RT constructs must be rewritten using threads --thread -- periodic(1000)(IncTime) end Timer \end{vdm_al} ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.34Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤*Eine klare Vorstellung vom Zielzustand |
|
2026-03-28