Theory Example
subsection ‹Example Bali program›
theory Example
imports Eval WellForm
begin
text ‹
The following example Bali program includes:
\begin{itemize}
\item class and interface declarations with inheritance, hiding of fields,
overriding of methods (with refined result type), array type,
\item method call (with dynamic binding), parameter access, return expressions,
\item expression statements, sequential composition, literal values,
local assignment, local access, field assignment, type cast,
\item exception generation and propagation, try and catch statement, throw
statement
\item instance creation and (default) static initialization
\end{itemize}
\begin{verbatim}
package java_lang
public interface HasFoo {
public Base foo(Base z);
}
public class Base implements HasFoo {
static boolean arr[] = new boolean[2];
public HasFoo vee;
public Base foo(Base z) {
return z;
}
}
public class Ext extends Base {
public int vee;
public Ext foo(Base z) {
((Ext)z).vee = 1;
return null;
}
}
public class Main {
public static void main(String args[]) throws Throwable {
Base e = new Ext();
try {e.foo(null); }
catch(NullPointerException z) {
while(Ext.arr[2]) ;
}
}
}
\end{verbatim}
›
declare widen.null [intro]
lemma wf_fdecl_def2: "⋀fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
apply (unfold wf_fdecl_def)
apply (simp (no_asm))
done
declare wf_fdecl_def2 [iff]
subsubsection "type and expression names"