# Theory Examples

```(*  Title:      Jinja/J/Examples.thy

Author:     Christoph Petzinger
*)

section ‹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))
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 "

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),
(''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
```