10
RML example: the Exp language
§Relation
eval
relation eval: Exp => int =
axiom eval(INTconst(ival)) =>
ival
rule eval(e1) => v1 &
eval(e2) => v2 & int_add(v1,v2) => v3
------------------------------------------------------
eval (PLUSop(e1,e2)) => v3
rule eval(e1) => v1 &
eval(e2) => v2 & int_sub(v1,v2) => v3
-----------------------------------------------------
eval (SUBop(e1,e2)) => v3
rule eval(e1) => v1 &
eval(e2) => v2 & int_mul(v1,v2) => v3
-----------------------------------------------------
eval (MULop(e1,e2)) => v3
rule eval(e1) => v1 &
eval(e2) => v2 & int_div(v1,v2) => v3
-----------------------------------------------------
eval (DIVop(e1,e2)) => v3
rule eval(e) => v1 &
int_neg(v1) => v2
-----------------------------------------------------
eval (NEGop(e)) => v2
end