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 sideeffecting 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{DvOCPE01}.\\ 
43 in \cite{DvOCPE01}.\\ 
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} 