| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMRT/oldcarradioRT/ (Wiener Entwicklungsmethode ©) Datei vom 13.4.2020 mit Größe 595 B |
|
Quelle RadioAdjustVolume.vdmrt Sprache: VDM |
|||||||||
|
\begin{vdm_al}
class RadioAdjustVolume is subclass of BasicTask operations public RadioAdjustVolume: EventDispatcher ==> RadioAdjustVolume RadioAdjustVolume (pde) == BasicTask("AdjustVolume",pde); -- we do not specify *what* the operation does -- we only specify its execution time public AdjustVolume: () ==> () AdjustVolume () == duration (100) skip; protected handleEvent: Event ==> () handleEvent (pe) == ( AdjustVolume(); -- send message to next task in this scenario sendMessage("UpdateScreenVolume", pe.getEvent()) ) end RadioAdjustVolume \end{vdm_al} ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28