Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/VDM/VDMPP/access-controlPP/ (Wiener Entwicklungsmethode ^©) Datei vom 13.4.2020 mit Größe 990 B

Quelle 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%

¤ 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.