Paper available on Hoare logic for Java

I am pleased to announce the availability of the following new paper:

	Axiomatic Semantics for Java_light
		David von Oheimb


We introduce a Hoare-style calculus for a nearly full subset of
sequential Java, which we call Java_light. 
This axiomatic semantics has been proved sound and complete 
wrt. our operational semantics of Java_light described earlier. 
The proofs also give new insights into the role of type-safety. 
All the formalization and proofs have been done with the 
theorem prover Isabelle/HOL.

To be presented at the
ECOOP2000 Workshop on Formal Techniques for Java Programs

Available under http://isabelle.in.tum.de/Bali/papers/ECOOP00.html

Comments are welcome.

	David von Oheimb