header {* \isaheader{Example Expressions} *}
theory Examples imports Expr begin
definition classObject::"J_mb cdecl"
where
"classObject == (''Object'','''',[],[])"
definition classI :: "J_mb cdecl"
where
"classI ==
(''I'', Object,
[],
[(''mult'',[Integer,Integer],Integer,[''i'',''j''],
if (Var ''i'' «Eq» Val(Intg 0)) (Val(Intg 0))
else Var ''j'' «Add»
Var this • ''mult''([Var ''i'' «Add» Val(Intg -1),Var ''j'']))
])"
definition classL :: "J_mb cdecl"
where
"classL ==
(''L'', Object,
[(''F'',Integer), (''N'',Class ''L'')],
[(''app'',[Class ''L''],Void,[''l''],
if (Var this • ''N''{''L''} «Eq» null)
(Var this • ''N''{''L''} := Var ''l'')
else (Var this • ''N''{''L''}) • ''app''([Var ''l'']))
])"
definition testExpr_BuildList :: "expr"
where
"testExpr_BuildList ==
{''l1'':Class ''L'' := new ''L'';
Var ''l1''•''F''{''L''} := Val(Intg 1);;
{''l2'':Class ''L'' := new ''L'';
Var ''l2''• ''F''{''L''} := Val(Intg 2);;
{''l3'':Class ''L'' := new ''L'';
Var ''l3''• ''F''{''L''} := Val(Intg 3);;
{''l4'':Class ''L'' := new ''L'';
Var ''l4''• ''F''{''L''} := Val(Intg 4);;
Var ''l1''•''app''([Var ''l2'']);;
Var ''l1''•''app''([Var ''l3'']);;
Var ''l1''•''app''([Var ''l4''])}}}}"
definition testExpr1 ::"expr"
where
"testExpr1 == Val(Intg 5)"
definition testExpr2 ::"expr"
where
"testExpr2 == BinOp (Val(Intg 5)) Add (Val(Intg 6))"
definition testExpr3 ::"expr"
where
"testExpr3 == BinOp (Var ''V'') Add (Val(Intg 6))"
definition testExpr4 ::"expr"
where
"testExpr4 == ''V'' := Val(Intg 6)"
definition testExpr5 ::"expr"
where
"testExpr5 == new ''Object'';; {''V'':(Class ''C'') := new ''C''; Var ''V''•''F''{''C''} := Val(Intg 42)}"
definition testExpr6 ::"expr"
where
"testExpr6 == {''V'':(Class ''I'') := new ''I''; Var ''V''•''mult''([Val(Intg 40),Val(Intg 4)])}"
definition mb_isNull:: "expr"
where
"mb_isNull == Var this • ''test''{''A''} «Eq» null "
definition mb_add:: "expr"
where
"mb_add == (Var this • ''int''{''A''} :=( Var this • ''int''{''A''} «Add» Var ''i''));; (Var this • ''int''{''A''})"
definition mb_mult_cond:: "expr"
where
"mb_mult_cond == (Var ''j'' «Eq» Val (Intg 0)) «Eq» Val (Bool False)"
definition mb_mult_block:: "expr"
where
"mb_mult_block == ''temp'':=(Var ''temp'' «Add» Var ''i'');;''j'':=(Var ''j'' «Add» Val (Intg -1))"
definition mb_mult:: "expr"
where
"mb_mult == {''temp'':Integer:=Val (Intg 0); While (mb_mult_cond) mb_mult_block;; ( Var this • ''int''{''A''} := Var ''temp'';; Var ''temp'' )}"
definition classA:: "J_mb cdecl"
where
"classA ==
(''A'', Object,
[(''int'',Integer),
(''test'',Class ''A'') ],
[(''isNull'',[],Boolean,[], mb_isNull),
(''add'',[Integer],Integer,[''i''], mb_add),
(''mult'',[Integer,Integer],Integer,[''i'',''j''], mb_mult) ])"
definition testExpr_ClassA:: "expr"
where
"testExpr_ClassA ==
{''A1'':Class ''A'':= new ''A'';
{''A2'':Class ''A'':= new ''A'';
{''testint'':Integer:= Val (Intg 5);
(Var ''A2''• ''int''{''A''} := (Var ''A1''• ''add''([Var ''testint''])));;
(Var ''A2''• ''int''{''A''} := (Var ''A1''• ''add''([Var ''testint''])));;
Var ''A2''• ''mult''([Var ''A2''• ''int''{''A''}, Var ''testint'']) }}}"
end