Quelle  Env.vdmpp

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