summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/NanoJava/document/root.tex

changeset 11477 | 4d042d3f957d |

parent 11376 | bf98ad1c22c6 |

child 11560 | 46d0bde121ab |

--- a/src/HOL/NanoJava/document/root.tex Wed Aug 08 12:36:48 2001 +0200 +++ b/src/HOL/NanoJava/document/root.tex Wed Aug 08 14:12:36 2001 +0200 @@ -36,7 +36,8 @@ language Java (with essentially just classes) derived from the one given in \cite{NipkowOP00}. For {\nJava}, an operational semantics is given as well as a Hoare logic, - which is proved both sound and (relatively) complete. The Hoare logic + which is proved both sound and (relatively) complete. + The Hoare logic supports side-effecting expressions and implements a new approach for handling auxiliary variables. A more complex Hoare logic covering a much larger subset of Java is described in \cite{DvO-CPE01}.\\