Quelle CONTEXT-liquid.vdmpp Sprache: VDM

class Liquid

instance variables
  protected aap : AtmosphericAirPressure;      -- static property
  protected boiling_point : map real to real;  -- static property
  protected temperature : real;                -- dynamic property
  protected amount : real;                     -- dynamic property

operations
  public
  GetAap: () ==> AtmosphericAirPressure
  GetAap() ==
    return aap;

  public
  SetAap: AtmosphericAirPressure ==> ()
  SetAap(a) ==
    aap := a;

  public
  GetBoilingPoint: real ==> real
  GetBoilingPoint(atm) ==
    return boiling_point(atm)
  pre atm in set dom boiling_point;

  public
  GetTemperature: () ==> real
  GetTemperature() ==
    return temperature;

  public
  SetTemperature: real ==> ()
  SetTemperature(t) ==
    temperature := t;

  public
  AddTemperature: () ==> ()
  AddTemperature() ==
    if temperature < boiling_point(aap.GetAtm())
      then
        temperature := temperature + 1.0
      else
       (temperature := boiling_point(aap.GetAtm());
        amount := amount - 1.0  --- evaporation (1.0 is inadequate value!)
       )
  pre
    aap.GetAtm() in set dom boiling_point and
    temperature <= boiling_point(aap.GetAtm())
  post
    temperature <= boiling_point(aap.GetAtm());

  pure public
  GetAmount: () ==> real
  GetAmount() ==
    return amount;

  public
  SetAmount: real ==> ()
  SetAmount(a) ==
    amount := a;

end Liquid

quality97%

¤ Dauer der Verarbeitung: 0.16 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.