| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMRT/oldcarradioRT/ (Wiener Entwicklungsmethode ©) Datei vom 13.4.2020 mit Größe 636 B |
|
Quelle MMIUpdateScreenAddress.vdmrt Sprache: VDM |
|||||||||
|
\begin{vdm_al}
class MMIUpdateScreenAddress is subclass of BasicTask operations public MMIUpdateScreenAddress: EventDispatcher ==> MMIUpdateScreenAddress MMIUpdateScreenAddress (pde) == BasicTask("UpdateScreenAddress",pde); public UpdateScreen: () ==> () UpdateScreen () == duration (500) skip; -- we do not specify *what* the operation does -- we only specify its execution time protected handleEvent: Event ==> () handleEvent (pe) == ( UpdateScreen(); -- scenario finished. signal response back to the environment raiseInterrupt("InsertAddress", pe.getEvent()) ) end MMIUpdateScreenAddress \end{vdm_al} ¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28