(* Title: HOL/Bali/Term.thy
Author: David von Oheimb
*)
subsection ‹Java expressions
and statements
›
theory Term imports Value Table
begin
text ‹
design issues:
\begin{itemize}
\item invocation frames
for local variables could be reduced
to special static
objects (one per method). This would reduce redundancy, but yield a rather
non-standard execution model more difficult
to understand.
\item method bodies separated
from calls
to handle assumptions
in axiomat.
semantics
NB: Body
is intended
to be
in the environment of the called method.
\item class initialization
is regarded as (auxiliary) statement
(required
for AxSem)
\item result expression of method return
is handled
by a special result variable
result variable
is treated uniformly
with local variables
\begin{itemize}
\item[+] welltypedness
and existence of the result/return expression
is
ensured without extra efford
\end{itemize}
\end{itemize}
simplifications:
\begin{itemize}
\item expression statement allowed
for any expression
\item This
is modeled as a special non-assignable
local variable
\item Super
is modeled as a general expression
with the same
value as This
\item access
to field x
in current
class via This.x
\item NewA creates only one-dimensional arrays;
initialization of further subarrays may be simulated
with nested NewAs
\item The
'Lit' constructor
is allowed
to contain a reference
value.
But this
is assumed
to be prohibited
in the input language, which
is enforced
by the type-checking rules.
\item a call of a static method via a type name may be simulated
by a dummy
variable
\item no nested blocks
with inner
local variables
\item no synchronized statements
\item no secondary forms of
if, while (e.g. no
for) (may be easily simulated)
\item no switch (may be simulated
with if)
\item the
‹try_catch_finally
› statement
is divided into the
‹try_catch
› statement
and a
finally statement, which may be considered as try..
finally with
empty catch
\item the
‹try_catch
› statement has exactly one catch clause;
multiple ones can be
simulated
with instanceof
\item the compiler
is supposed
to add the annotations {
‹_
›} during
type-checking. This
transformation
is left out as its result
is checked
by the type rules anyway
\end{itemize}
›
type_synonym locals =
"(lname, val) table" 🍋 ‹local variables
›
datatype jump
= Break label
🍋 ‹break
›
| Cont label
🍋 ‹continue
›
| Ret
🍋 ‹return
from method
›
datatype xcpt
🍋 ‹exception
›
= Loc loc
🍋 ‹location of allocated execption object
›
| Std xname
🍋 ‹intermediate standard exception, see Eval.thy
›
datatype error
= AccessViolation
🍋 ‹Access
to a member that isn
't permitted\
| CrossMethodJump
🍋 ‹Method exits
with a break or continue
›
datatype abrupt
🍋 ‹abrupt completion
›
= Xcpt xcpt
🍋 ‹exception
›
| Jump jump
🍋 ‹break, continue, return
›
| Error error
🍋 ‹runtime errors, we wan
't to detect and proof absent
in welltyped programms
›
type_synonym
abopt =
"abrupt option"
text ‹Local variable store
and exception.
Anticipation of State.thy used
by smallstep semantics.
For a method call,
we save the
local variables of the caller
in the
term Callee
to restore them
after method return.
Also an exception must be restored after the
finally
statement
›
translations
(type)
"locals" <= (type)
"(lname, val) table"
datatype inv_mode
🍋 ‹invocation mode
for method calls
›
= Static
🍋 ‹static
›
| SuperM
🍋 ‹super
›
| IntVir
🍋 ‹interface or virtual
›
record sig =
🍋 ‹signature of a method, cf. 8.4.2
›
name ::
"mname" 🍋 ‹acutally belongs
to Decl.thy
›
parTs::
"ty list"
translations
(type)
"sig" <= (type)
"\name::mname,parTs::ty list\"
(type)
"sig" <= (type)
"\name::mname,parTs::ty list,\::'a\"
🍋 ‹function codes
for unary operations
›
datatype unop = UPlus
🍋 ‹{
\tt +} unary plus
›
| UMinus
🍋 ‹{
\tt -} unary minus
›
| UBitNot
🍋 ‹{
\tt ~} bitwise NOT
›
| UNot
🍋 ‹{
\tt !} logical complement
›
🍋 ‹function codes
for binary operations
›
datatype binop = Mul
🍋 ‹{
\tt *} multiplication
›
| Div
🍋 ‹{
\tt /} division
›
| Mod
🍋 ‹{
\tt \%} remainder
›
| Plus
🍋 ‹{
\tt +} addition
›
| Minus
🍋 ‹{
\tt -} subtraction
›
| LShift
🍋 ‹{
\tt <<} left shift
›
| RShift
🍋 ‹{
\tt >>} signed right shift
›
| RShiftU
🍋 ‹{
\tt >>>} unsigned right shift
›
| Less
🍋 ‹{
\tt <} less than
›
| Le
🍋 ‹{
\tt <=} less than or equal
›
| Greater
🍋 ‹{
\tt >} greater than
›
| Ge
🍋 ‹{
\tt >=} greater than or equal
›
| Eq
🍋 ‹{
\tt ==} equal
›
| Neq
🍋 ‹{
\tt !=} not equal
›
| BitAnd
🍋 ‹{
\tt \&} bitwise
AND›
|
And 🍋 ‹{
\tt \&} boolean
AND›
| BitXor
🍋 ‹{
\texttt \^} bitwise Xor
›
| Xor
🍋 ‹{
\texttt \^} boolean Xor
›
| BitOr
🍋 ‹{
\tt |} bitwise Or
›
| Or
🍋 ‹{
\tt |} boolean Or
›
| CondAnd
🍋 ‹{
\tt \&\&} conditional
And›
| CondOr
🍋 ‹{
\tt ||} conditional Or
›
text‹The boolean operators {
\tt \&}
and {
\tt |} strictly evaluate both
of their arguments. The conditional operators {
\tt \&\&}
and {
\tt ||} only
evaluate the second argument
if the
value of the whole expression isn
't
allready determined
by the first argument.
e.g.: {
\tt false
\&\& e} e
is not evaluated;
{
\tt true || e} e
is not evaluated;
›
datatype var
= LVar lname
🍋 ‹local variable (incl. parameters)
›
| FVar qtname qtname bool expr vname (
‹{_,_,_}_.._
›[10,10,10,85,99]90)
🍋 ‹class field
›
🍋 ‹🍋‹{accC,statDeclC,stat}e..fn
››
🍋 ‹‹accC
›: accessing
class (static
class were
›
🍋 ‹the code
is declared. Annotation only needed
for›
🍋 ‹evaluation
to check accessibility)
›
🍋 ‹‹statDeclC
›: static
declaration class of field
›
🍋 ‹‹stat
›: static or
instance field?
›
🍋 ‹‹e
›: reference
to object
›
🍋 ‹‹fn
›: field name
›
| AVar expr expr (
‹_.[_]
›[90,10 ]90)
🍋 ‹array component
›
🍋 ‹🍋‹e1.[e2]
›: e1 array reference; e2 index
›
| InsInitV stmt var
🍋 ‹insertion of initialization before evaluation
›
🍋 ‹of var (technical
term for smallstep semantics.)
›
and expr
= NewC qtname
🍋 ‹class instance creation
›
| NewA ty expr (
‹New _[_]
›[99,10 ]85)
🍋 ‹array creation
›
| Cast ty expr
🍋 ‹type cast
›
| Inst expr ref_ty (
‹_ InstOf _
›[85,99] 85)
🍋 ‹instanceof
›
| Lit val
🍋 ‹literal
value, references not allowed
›
| UnOp unop expr
🍋 ‹unary operation
›
| BinOp binop expr expr
🍋 ‹binary operation
›
| Super
🍋 ‹special Super keyword
›
| Acc var
🍋 ‹variable access
›
| Ass var expr (
‹_:=_
› [90,85 ]85)
🍋 ‹variable assign
›
| Cond expr expr expr (
‹_ ? _ : _
› [85,85,80]80)
🍋 ‹conditional
›
| Call qtname ref_ty inv_mode expr mname
"(ty list)" "(expr list)"
(
‹{_,_,_}_
⋅_
'( {_}_')
›[10,10,10,85,99,10,10]85)
🍋 ‹method call
›
🍋 ‹🍋‹{accC,statT,mode}e
⋅mn({pTs}args)
› "\
🍋 ‹‹accC
›: accessing
class (static
class were
›
🍋 ‹the call code
is declared. Annotation only needed
for›
🍋 ‹evaluation
to check accessibility)
›
🍋 ‹‹statT
›: static
declaration class/interface of
›
🍋 ‹method
›
🍋 ‹‹mode
›: invocation mode
›
🍋 ‹‹e
›: reference
to object
›
🍋 ‹‹mn
›: field name
›
🍋 ‹‹pTs
›:
types of parameters
›
🍋 ‹‹args
›: the actual parameters/arguments
›
| Methd qtname sig
🍋 ‹(folded) method (see below)
›
| Body qtname stmt
🍋 ‹(unfolded) method body
›
| InsInitE stmt expr
🍋 ‹insertion of initialization before
›
🍋 ‹evaluation of expr (technical
term for smallstep sem.)
›
| Callee locals expr
🍋 ‹save callers locals
in callee-Frame
›
🍋 ‹(technical
term for smallstep semantics)
›
and stmt
= Skip
🍋 ‹empty statement
›
| Expr expr
🍋 ‹expression statement
›
| Lab jump stmt (
‹_
∙ _
› [ 99,66]66)
🍋 ‹labeled statement; handles break
›
| Comp stmt stmt (
‹_;; _
› [ 66,65]65)
|
If' expr stmt stmt (\If'(_
') _ Else _\ [ 80,79,79]70)
| Loop label expr stmt (
‹_
∙ While
'(_') _
› [ 99,80,79]70)
| Jmp jump
🍋 ‹break, continue, return
›
| Throw expr
| TryC stmt qtname vname stmt (
‹Try _ Catch
'(_ _') _
› [79,99,80,79]70)
🍋 ‹🍋‹Try c1 Catch(C vn) c2
››
🍋 ‹‹c1
›: block were exception may be thrown
›
🍋 ‹‹C
›: execption
class to catch
›
🍋 ‹‹vn
›:
local name
for exception used
in ‹c2
››
🍋 ‹‹c2
›: block
to execute when exception
is cateched
›
| Fin stmt stmt (
‹_
Finally _
› [ 79,79]70)
| FinA abopt stmt
🍋 ‹Save abruption of first statement
›
🍋 ‹technical
term for smallstep sem.)
›
| Init qtname
🍋 ‹class initialization
›
datatype_compat var expr stmt
text ‹
The expressions Methd
and Body are artificial program constructs,
in the
sense that they are not used
to define a concrete Bali program.
In the
operational semantic
's they are "generated on the fly"
to decompose the task
to define the behaviour of the Call expression.
They are crucial
for the axiomatic semantics
to give a syntactic hook
to insert
some assertions (cf. AxSem.thy, Eval.thy).
The Init statement (
to initialize a
class on its first
use)
is
inserted
in various places
by the semantics.
Callee, InsInitV, InsInitE,FinA are only needed as intermediate steps
in the
smallstep (transition) semantics (cf. Trans.thy). Callee
is used
to save the
local variables of the caller
for method return. So ve avoid modelling a
frame stack.
The InsInitV/E terms are only used
by the smallstep semantics
to model the
intermediate steps of class-initialisation.
›
type_synonym "term" =
"(expr+stmt,var,expr list) sum3"
translations
(type)
"sig" <= (type)
"mname \ ty list"
(type)
"term" <= (type)
"(expr+stmt,var,expr list) sum3"
abbreviation this :: expr
where "this == Acc (LVar This)"
abbreviation LAcc ::
"vname \ expr" (
‹!!
›)
where "!!v == Acc (LVar (EName (VNam v)))"
abbreviation
LAss ::
"vname \ expr \stmt" (
‹_:==_
› [90,85] 85)
where "v:==e == Expr (Ass (LVar (EName (VNam v))) e)"
abbreviation
Return ::
"expr \ stmt"
where "Return e == Expr (Ass (LVar (EName Res)) e);; Jmp Ret" 🍋 ‹\tt Res := e;; Jmp Ret
›
abbreviation
StatRef ::
"ref_ty \ expr"
where "StatRef rt == Cast (RefT rt) (Lit Null)"
definition
is_stmt ::
"term \ bool"
where "is_stmt t = (\c. t=In1r c)"
ML
‹ML_Thms.bind_thms (
"is_stmt_rews", sum3_instantiate
🍋 @{
thm is_stmt_def})
›
declare is_stmt_rews [simp]
text ‹
Here
is some syntactic stuff
to handle the injections of statements,
expressions, variables
and expression lists into general terms.
›
abbreviation (input)
expr_inj_term ::
"expr \ term" (
‹⟨_
⟩🚫e
› 1000)
where "\e\\<^sub>e == In1l e"
abbreviation (input)
stmt_inj_term ::
"stmt \ term" (
‹⟨_
⟩🚫s
› 1000)
where "\c\\<^sub>s == In1r c"
abbreviation (input)
var_inj_term ::
"var \ term" (
‹⟨_
⟩🚫v
› 1000)
where "\v\\<^sub>v == In2 v"
abbreviation (input)
lst_inj_term ::
"expr list \ term" (
‹⟨_
⟩🚫l
› 1000)
where "\es\\<^sub>l == In3 es"
text ‹It seems
to be more elegant
to have an
overloaded injection like the
following.
›
class inj_term =
fixes inj_term::
"'a \ term" (
‹⟨_
⟩› 1000)
text ‹How this
overloaded injections work can be seen
in the
theory
‹DefiniteAssignment
›. Other big
inductive relations on
terms defined
in theories
‹WellType
›,
‹Eval
›,
‹Evaln
› and
‹AxSem
› don
't follow this convention right now, but introduce subtle
syntactic sugar
in the relations themselves
to make a distinction on
expressions, statements
and so on. So unfortunately you will encounter a
mixture of dealing
with these injections. The abbreviations above are used
as bridge between the different conventions.
›
instantiation stmt :: inj_term
begin
definition
stmt_inj_term_def:
"\c::stmt\ = In1r c"
instance ..
end
lemma stmt_inj_term_simp:
"\c::stmt\ = In1r c"
by (simp add: stmt_inj_term_def)
lemma stmt_inj_term [iff]:
"\x::stmt\ = \y\ \ x = y"
by (simp add: stmt_inj_term_simp)
instantiation expr :: inj_term
begin
definition
expr_inj_term_def:
"\e::expr\ = In1l e"
instance ..
end
lemma expr_inj_term_simp:
"\e::expr\ = In1l e"
by (simp add: expr_inj_term_def)
lemma expr_inj_term [iff]:
"\x::expr\ = \y\ \ x = y"
by (simp add: expr_inj_term_simp)
instantiation var :: inj_term
begin
definition
var_inj_term_def:
"\v::var\ = In2 v"
instance ..
end
lemma var_inj_term_simp:
"\v::var\ = In2 v"
by (simp add: var_inj_term_def)
lemma var_inj_term [iff]:
"\x::var\ = \y\ \ x = y"
by (simp add: var_inj_term_simp)
class expr_of =
fixes expr_of ::
"'a \ expr"
instantiation expr :: expr_of
begin
definition
"expr_of = (\(e::expr). e)"
instance ..
end
instantiation list :: (expr_of) inj_term
begin
definition
"\es::'a list\ = In3 (map expr_of es)"
instance ..
end
lemma expr_list_inj_term_def:
"\es::expr list\ \ In3 es"
by (simp add: inj_term_list_def expr_of_expr_def)
lemma expr_list_inj_term_simp:
"\es::expr list\ = In3 es"
by (simp add: expr_list_inj_term_def)
lemma expr_list_inj_term [iff]:
"\x::expr list\ = \y\ \ x = y"
by (simp add: expr_list_inj_term_simp)
lemmas inj_term_simps = stmt_inj_term_simp expr_inj_term_simp var_inj_term_simp
expr_list_inj_term_simp
lemmas inj_term_sym_simps = stmt_inj_term_simp [
THEN sym]
expr_inj_term_simp [
THEN sym]
var_inj_term_simp [
THEN sym]
expr_list_inj_term_simp [
THEN sym]
lemma stmt_expr_inj_term [iff]:
"\t::stmt\ \ \w::expr\"
by (simp add: inj_term_simps)
lemma expr_stmt_inj_term [iff]:
"\t::expr\ \ \w::stmt\"
by (simp add: inj_term_simps)
lemma stmt_var_inj_term [iff]:
"\t::stmt\ \ \w::var\"
by (simp add: inj_term_simps)
lemma var_stmt_inj_term [iff]:
"\t::var\ \ \w::stmt\"
by (simp add: inj_term_simps)
lemma stmt_elist_inj_term [iff]:
"\t::stmt\ \ \w::expr list\"
by (simp add: inj_term_simps)
lemma elist_stmt_inj_term [iff]:
"\t::expr list\ \ \w::stmt\"
by (simp add: inj_term_simps)
lemma expr_var_inj_term [iff]:
"\t::expr\ \ \w::var\"
by (simp add: inj_term_simps)
lemma var_expr_inj_term [iff]:
"\t::var\ \ \w::expr\"
by (simp add: inj_term_simps)
lemma expr_elist_inj_term [iff]:
"\t::expr\ \ \w::expr list\"
by (simp add: inj_term_simps)
lemma elist_expr_inj_term [iff]:
"\t::expr list\ \ \w::expr\"
by (simp add: inj_term_simps)
lemma var_elist_inj_term [iff]:
"\t::var\ \ \w::expr list\"
by (simp add: inj_term_simps)
lemma elist_var_inj_term [iff]:
"\t::expr list\ \ \w::var\"
by (simp add: inj_term_simps)
lemma term_cases:
"
[∧ v. P
⟨v
⟩🚫v;
∧ e. P
⟨e
⟩🚫e;
∧ c. P
⟨c
⟩🚫s;
∧ l. P
⟨l
⟩🚫l
]
==> P t
"
apply (cases t)
apply (rename_tac a, case_tac a)
apply auto
done
subsubsection
‹Evaluation of unary operations
›
primrec eval_unop ::
"unop \ val \ val"
where
"eval_unop UPlus v = Intg (the_Intg v)"
|
"eval_unop UMinus v = Intg (- (the_Intg v))"
|
"eval_unop UBitNot v = Intg 42" 🍋 ‹FIXME: Not yet implemented
›
|
"eval_unop UNot v = Bool (\ the_Bool v)"
subsubsection
‹Evaluation of binary operations
›
primrec eval_binop ::
"binop \ val \ val \ val"
where
"eval_binop Mul v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))"
|
"eval_binop Div v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
|
"eval_binop Mod v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
|
"eval_binop Plus v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
|
"eval_binop Minus v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
🍋 ‹Be aware of the explicit coercion of the shift distance
to nat
›
|
"eval_binop LShift v1 v2 = Intg ((the_Intg v1) * (2^(nat (the_Intg v2))))"
|
"eval_binop RShift v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
|
"eval_binop RShiftU v1 v2 = Intg 42" 🍋 ‹FIXME: Not yet implemented
›
|
"eval_binop Less v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))"
|
"eval_binop Le v1 v2 = Bool ((the_Intg v1) \ (the_Intg v2))"
|
"eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
|
"eval_binop Ge v1 v2 = Bool ((the_Intg v2) \ (the_Intg v1))"
|
"eval_binop Eq v1 v2 = Bool (v1=v2)"
|
"eval_binop Neq v1 v2 = Bool (v1\v2)"
|
"eval_binop BitAnd v1 v2 = Intg 42" 🍋 ‹FIXME: Not yet implemented
›
|
"eval_binop And v1 v2 = Bool ((the_Bool v1) \ (the_Bool v2))"
|
"eval_binop BitXor v1 v2 = Intg 42" 🍋 ‹FIXME: Not yet implemented
›
|
"eval_binop Xor v1 v2 = Bool ((the_Bool v1) \ (the_Bool v2))"
|
"eval_binop BitOr v1 v2 = Intg 42" 🍋 ‹FIXME: Not yet implemented
›
|
"eval_binop Or v1 v2 = Bool ((the_Bool v1) \ (the_Bool v2))"
|
"eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \ (the_Bool v2))"
|
"eval_binop CondOr v1 v2 = Bool ((the_Bool v1) \ (the_Bool v2))"
definition
need_second_arg ::
"binop \ val \ bool" where
"need_second_arg binop v1 = (\ ((binop=CondAnd \ \ the_Bool v1) \
(binop=CondOr
∧ the_Bool v1)))
"
text ‹🍋‹CondAnd
› and 🍋‹CondOr
› only evalulate the second argument
if the
value isn
't already determined by the first argument\
lemma need_second_arg_CondAnd [simp]:
"need_second_arg CondAnd (Bool b) = b"
by (simp add: need_second_arg_def)
lemma need_second_arg_CondOr [simp]:
"need_second_arg CondOr (Bool b) = (\ b)"
by (simp add: need_second_arg_def)
lemma need_second_arg_strict[simp]:
"\binop\CondAnd; binop\CondOr\ \ need_second_arg binop b"
by (cases binop)
(simp_all add: need_second_arg_def)
end
