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

*Bot Zugriff

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.