| products/sources/formale Sprachen/VDM/VDMPP/SAFERPP/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: root.tex Sprache: VDMOriginal von: VDM© |
|
||||||
|
\section{HandControlUnit Class}
\begin{vdm_al} class HandControlUnit types public Button = <Up> | <Down>; public Mode = <Tran> | <Rot>; instance variables x : Command`Direction; pitch : Command`Direction; yaw_y : Command`Direction; roll_z : Command`Direction; aahbutton : Button; modeswitch : Mode; operations public SetAAH : Button ==> () SetAAH(aahbuttonarg) == aahbutton := aahbuttonarg; public ReadAAH : () ==> Button ReadAAH() == return aahbutton; public SetGrip : Command`Direction * Command`Direction * Command`Direction * Command`Direction ==> () SetGrip(xarg, pitcharg, yaw_yarg, roll_zarg) == (x := xarg; pitch := pitcharg; yaw_y := yaw_yarg; roll_z := roll_zarg); public SetMode : Mode ==> () SetMode(m) == modeswitch := m; public ReadGrip : () ==> Command`Direction * Command`Direction * Command`Direction * Command`Direction * Mode ReadGrip() == return mk_(x, pitch, yaw_y, roll_z, modeswitch); end HandControlUnit \end{vdm_al} The test coverage table for the HandControlUnit class looks like: \begin{rtinfo}{vdm.tc}[HandControlUnit] \end{rtinfo} ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
