| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/VDMPP/KLVPP/ Datei vom 13.4.2020 mit Größe 706 B |
|
Quellcode-Bibliothek EmergencyBreak.vdmpp Sprache: VDM |
|||||||||
|
\section{The EmergencyBreak Class}
The EmergencyBreak class models the emergency break of a train. The instance variable maintains the state of the emergency break. There are operations for setting and unsetting the emergency break, and for getting the status of it. \begin{vdm_al} class EmergencyBreak instance variables emergencybreak : bool := false; operations public setEmergencyBreak : () ==> () setEmergencyBreak () == emergencybreak := true; public unsetEmergencyBreak : () ==> () unsetEmergencyBreak () == emergencybreak := false; pure public getEmergencyBreak : () ==> bool getEmergencyBreak () == return emergencybreak; end EmergencyBreak \end{vdm_al} ¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.1Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
