Quellcode-Bibliothek Env.vdmpp Sprache: VDM

class Env

instance variables

senv : map FExp`Id to FExp`SType;
denv : map FExp`Id to FExp`Val;

operations

public Env: map FExp`Id to FExp`SType * map FExp`Id to FExp`Val ==> Env
Env(s,d) ==
  (senv := s;
   denv := d;
  );

public GetSenv: () ==> map FExp`Id to FExp`SType
GetSenv() ==
  return senv;

public GetDenv: () ==> map FExp`Id to FExp`Val
GetDenv() ==
  return denv;

pure public GetVal: FExp`Id ==> FExp`Val
GetVal(id) ==
  return denv(id)
pre id in set dom denv;

public GetAVal:FExp`Id * FExp`Id ==> FExp`Val
GetAVal(id,index) ==
  return denv(id)(index)
pre id in set dom denv and index in set dom denv(id);

public GetSType: FExp`Id ==> FExp`SType
GetSType(id) ==
  return senv(id)
pre id in set dom denv;

public GetSAType: FExp`Id ==> FExp`AType
GetSAType(id) ==
  return senv(id)
pre id in set dom denv;

public GetAType:FExp`Id * FExp`Id ==> FExp`SType
GetAType(id,index) ==
  return senv(id)(index)
pre id in set dom denv and index in set dom denv(id);

end Env

quality100%

¤ 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.15Bemerkung: (vorverarbeitet) ¤

Versionsinformation zu Columbo

Bemerkung:

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders