equal
deleted
inserted
replaced
34 \begin{abstract}\noindent |
34 \begin{abstract}\noindent |
35 These theories define {\nJava}, a very small fragment of the programming |
35 These theories define {\nJava}, a very small fragment of the programming |
36 language Java (with essentially just classes) derived from the one given |
36 language Java (with essentially just classes) derived from the one given |
37 in \cite{NipkowOP00}. |
37 in \cite{NipkowOP00}. |
38 For {\nJava}, an operational semantics is given as well as a Hoare logic, |
38 For {\nJava}, an operational semantics is given as well as a Hoare logic, |
39 which is proved both sound and (relatively) complete. The Hoare logic |
39 which is proved both sound and (relatively) complete. |
|
40 The Hoare logic supports side-effecting expressions and |
40 implements a new approach for handling auxiliary variables. |
41 implements a new approach for handling auxiliary variables. |
41 A more complex Hoare logic covering a much larger subset of Java is described |
42 A more complex Hoare logic covering a much larger subset of Java is described |
42 in \cite{DvO-CPE01}.\\ |
43 in \cite{DvO-CPE01}.\\ |
43 See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}. |
44 See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}. |
44 \end{abstract} |
45 \end{abstract} |