Theory Term
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"
datatype jump
= Break label
| Cont label
| Ret
datatype xcpt
= Loc loc
| Std xname
datatype error
= AccessViolation
| CrossMethodJump
datatype abrupt
= Xcpt xcpt
| Jump jump
| Error error
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"