Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: FExp.vdmpp Sprache: VDM

Original von: VDM^©

class FExp

instance variables

fexp : Expr;

operations

public FExp : Expr ==> FExp
FExp(fe) ==
fexp := fe;

public GetExp: () ==> Expr
GetExp() ==
 return fexp;

types

public AtomicVal = bool | int | <Indet>;
public BoolArray = map Id to bool;
public IntArray = map Id to int;
public UnArray = map Id to <Indet>;
public StructuredVal = BoolArray | IntArray | UnArray;
public Val = AtomicVal | StructuredVal;

public Expr = Id | UnId | BoolExpr | ArithExpr | ArrayLookup;

public Id = token;

public UnId :: <requester>|<resource>; --<action>;

-- Expressions returning true or false
public BoolExpr = RelExpr | Unary | Infix | Equal | boolLiteral;

public RelExpr :: left : Expr
 op : <LT>|<GT>
 right : Expr;

public Unary :: op : <NOT>
 body : Expr;

public Infix :: left : Expr
 op : <AND>|<OR>
 right : Expr;

public Equal :: left : Expr
 op : <EQ>
 right : Expr;

public boolLiteral :: <TRUE>|<FALSE>;

-- Expression returning integer
public ArithExpr = intLiteral; -- | ArithInfix

public intLiteral :: <ZERO>|<ONE>|<TWO>|<THREE>|<FOUR>|<FIVE>|<SIX>|<SEVEN>|<EIGHT>|<NINE>|<TEN>;

public ArrayLookup :: aname : Id | UnId
 index : Id | UnId;

operations

-- binds the unbound variables within an expression.

public BindExpr: Expr * Request ==> FExp`Expr
BindExpr(fe,req) ==
cases fe:
 mk_UnId(<requester>) -> return req.GetSubject(),
 mk_UnId(<resource>) -> return req.GetResource(),
 mk_RelExpr(left,op,right) -> return mk_RelExpr(BindExpr(left,req), op, BindExpr(right,req)),
 mk_Unary(op,body) -> return mk_Unary(op,BindExpr(body,req)),
 mk_Infix(left,op,right) -> return mk_Infix(BindExpr(left,req), op, BindExpr(right,req)),
--mk_ArrExp(left,op,right) -> ...
 mk_intLiteral(-) -> return fe,
 mk_boolLiteral(-) -> return fe,
 mk_ArrayLookup(aname,index) -> return mk_ArrayLookup(BindExpr(aname,req),BindExpr(index,req)),
 others -> return fe
end;

-- Evaluate returns the meaning of an expression, wrt an environment

---------------------------------------
-- Dynamic Semantics for Expressions --
---------------------------------------

public EvaluateBind : Request * Env ==> Val
EvaluateBind(req,env) ==
 let expr = BindExpr(fexp,req) in
 Evaluate(expr,env);

Evaluate : Expr * Env ==> Val
Evaluate(expr,env) ==
 cases expr :
 mk_RelExpr(-,-,-) -> MRelExpr(expr,env),
 mk_Unary(-,-) -> MUnary(expr,env),
 mk_Infix(-,-,-) -> MInfix(expr,env),
 mk_Equal(-,-,-) -> MEqual(expr,env),
--mk_ArrExp(-,-,-) -> ...
 mk_boolLiteral(-) -> MLiteral(expr),
 mk_intLiteral(-) -> MLiteral(expr),
 mk_ArrayLookup(-,-) -> MArrayLookup(expr,env),
 others -> MId(expr,env)
 end;

pure private MId : Id * Env ==> Val
MId(Id,env) ==
return env.GetVal(Id);

MRelExpr : RelExpr * Env ==> Val
MRelExpr(exp,env) ==
 cases exp:
 mk_RelExpr(-,<GT>,-) -> return (EvaluateGT(exp.left,exp.right,env)),
 mk_RelExpr(-,<LT>,-) -> return (EvaluateLT(exp.left,exp.right,env)),
 others -> error
 end;

EvaluateLT: Expr * Expr * Env ==> Val
EvaluateLT(exp1,exp2,env) ==
 return (Evaluate(exp1,env) < Evaluate(exp2,env));

EvaluateGT: Expr * Expr * Env ==> Val
EvaluateGT(exp1,exp2,env) ==
 return (Evaluate(exp1,env) > Evaluate(exp2,env));

MUnary : Unary * Env ==> Val
MUnary(unary,env) ==
return not (Evaluate(unary.body,env));

MInfix : Infix * Env ==> Val
MInfix(exp,env) ==
 cases exp:
 mk_Infix(-,<AND>,-) -> return (EvaluateAND(exp.left,exp.right,env)),
 mk_Infix(-,<OR>,-) -> return (EvaluateOR(exp.left,exp.right,env)),
 others -> error
 end;

EvaluateAND: Expr * Expr * Env ==> Val
EvaluateAND(exp1,exp2,env) ==
 return (Evaluate(exp1,env) and Evaluate(exp2,env));

MEqual : Equal * Env ==> Val
MEqual(exp,env) ==
 return (Evaluate(exp.left, env) = Evaluate(exp.right,env));

-- order of evaluation is left to right, as stipulated by XACML standard

EvaluateOR: Expr * Expr * Env ==> Val
EvaluateOR(exp1,exp2,env) ==
 if (Evaluate(exp1,env))
 then return true
 else return Evaluate(exp2,env);

MArrayLookup : ArrayLookup * Env ==> Val
MArrayLookup(mk_ArrayLookup(aname,index),env) ==
 return (MId(aname,env))(index)
pre index in set dom MId(aname,env);

functions

MLiteral : boolLiteral | intLiteral -> Val
MLiteral(exp) ==
 cases exp:
 mk_boolLiteral(<TRUE>) -> true,
 mk_boolLiteral(<FALSE>)-> false,
 mk_intLiteral(<ZERO>) -> 0,
 mk_intLiteral(<ONE>) -> 1,
 mk_intLiteral(<TWO>) -> 2,
 mk_intLiteral(<THREE>) -> 3,
 mk_intLiteral(<FOUR>) -> 4,
 mk_intLiteral(<FIVE>) -> 5,
 mk_intLiteral(<SIX>) -> 6,
 mk_intLiteral(<SEVEN>) -> 7,
 mk_intLiteral(<EIGHT>) -> 8,
 mk_intLiteral(<NINE>) -> 9,
 others -> 10
 end;

--------------------------------------
-- Static Semantics for Expressions --
--------------------------------------

-- types for TP and WF judgements

types

public SType = |||AType|<Err>;

public AType = map Id to ||;

operations -- for TP and WF judgements

public wfExpr : Env ==> bool
wfExpr(env) ==
 return exprTp(fexp,env) = ;

private exprTp : Expr * Env ==> SType
exprTp(ex, env) ==
 cases ex:
 mk_Unary(-,-) -> wfUnary(ex,env),
 mk_Infix(-,-,-) -> wfInfix(ex,env),
 mk_RelExpr(-,-,-) -> wfRelExpr(ex,env),
-- mk_ArithExpr()
 mk_Equal(-,-,-) -> wfEqual(ex,env),
 mk_boolLiteral(-) -> wfLiteral(ex),
 mk_intLiteral(-) -> wfLiteral(ex),
 mk_UnId(-) -> wfUnId(ex),
 mk_ArrayLookup(-,-) -> wfArrayLookup(ex,env),
 others -> wfId(ex,env)
 end;

private wfInfix : Infix * Env ==> SType
wfInfix(mk_Infix(e1,-,e2), env) ==
 if exprTp(e1, env) = and exprTp(e2, env) = 
 then return 
 else return <Err>;

private wfUnary : Unary * Env ==> SType
wfUnary(mk_Unary(-,e), env) ==
 if exprTp(e, env) = 
 then return 
 else return <Err>;

private wfRelExpr : RelExpr * Env ==> SType
wfRelExpr(mk_RelExpr(e1,-,e2), env) ==
 if exprTp(e1, env) = and exprTp(e2, env) = 
 then return 
 else return <Err>;

private wfLiteral : boolLiteral | intLiteral ==> SType
wfLiteral(e) ==
 cases e:
 mk_boolLiteral(-) -> return ,
 mk_intLiteral(-) -> return ,
 others -> return <Err>
 end;

private wfEqual: Equal * Env ==> SType
wfEqual(mk_Equal(e1,-,e2), env) ==
 if (exprTp(e1, env) = and exprTp(e2, env) = ) or
 (exprTp(e1, env) = and exprTp(e2, env) = ) or
 (exprTp(e1, env) = and exprTp(e2, env) = )
 then return 
 else return <Err>;

private wfId: Id * Env ==> SType
wfId(e,env) ==
 if (e in set dom env.GetSenv())
 then let tp = env.GetSType(e) in
 if tp = or tp = or tp = 
 then return env.GetSType(e)
 else return <Err>
 else return <Err>;

wfUnId : UnId ==> SType
wfUnId(e) ==
 cases e:
 mk_UnId(<requester>) -> return ,
 mk_UnId(<resource>) -> return ,
-- mk_UnId(<action>) -> return ,
 others -> return <Err>
 end;

wfArrayLookup : ArrayLookup * Env ==> SType
wfArrayLookup(mk_ArrayLookup(id, index),env) ==
 if (id in set dom env.GetSenv()) -- Id is in the env
 then let tp = env.GetSType(id) in -- get the type of Id in env
 if tp = or tp = or tp = 
 then return <Err> -- Id is not an array in the env
 elseif index in set dom env.GetSenv()(id) -- assuming Id points to an array in senv
 then return env.GetAType(id,index) -- Get type of index in map
 else return <Err>
 else return <Err>;

end FExp

¤ Dauer der Verarbeitung: 0.32 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.