Theory Example
section ‹Example MicroJava Program›
theory Example imports SystemClasses Eval begin
text ‹
The following example MicroJava program includes:
class declarations with inheritance, hiding of fields, and overriding of
methods (with refined result type),
instance creation, local assignment, sequential composition,
method call with dynamic binding, literal values,
expression statement, local access, type cast, field assignment (in part),
skip.
\begin{verbatim}
class Base {
boolean vee;
Base foo(Base x) {return x;}
}
class Ext extends Base {
int vee;
Ext foo(Base x) {((Ext)x).vee=1; return null;}
}
class Example {
public static void main (String args[]) {
Base e=new Ext();
e.foo(null);
}
}
\end{verbatim}
›
datatype cnam' = Base' | Ext'