Quelle ValveDriveAssembly.vdmpp Sprache: VDM

\section{ValveDriveAssembly Class}

\begin{vdm_al}
class ValveDriveAssembly

instance variables
  thrusters : map ThrusterControl`ThrusterPosition to Thruster :=
    {thr |-> new Thruster() | thr in set ThrusterControl`ThrusterSet};

operations
  public
  UpdateThrusters : set of ThrusterControl`ThrusterPosition ==> ()
  UpdateThrusters(selected) ==
    (for all a in set selected
     do thrusters(a).SetOn();
     for all a in set ThrusterControl`ThrusterSet\selected
     do thrusters(a).SetOff());

  public
  ThrustersOn : () ==> set of ThrusterControl`ThrusterPosition
  ThrustersOn() ==
    return {thr | thr in set ThrusterControl`ThrusterSet &
            thrusters(thr).GetState() = <On>}

end ValveDriveAssembly
\end{vdm_al}

The test coverage table for the ValveDriveAssembly class looks like:

\begin{rtinfo}{vdm.tc}[ValveDriveAssembly]
\end{rtinfo}

quality97%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.