Paper available on Hoare logic for Java

• To: types@cis.upenn.edu
• Subject: Paper available on Hoare logic for Java
• From: David von Oheimb <oheimb@informatik.tu-muenchen.de>
• Date: Wed, 19 Apr 2000 17:59:52 +0000
• Organization: Technische =?iso-8859-1?Q?Universit=E4t=20M=FCnchen?= (TUM)
• Reply-To: oheimb@sunbroy49.informatik.tu-muenchen.de
• Sender: oheimb@informatik.tu-muenchen.de

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

	Axiomatic Semantics for Java_light
		David von Oheimb

Abstract

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
_____________________________
http://www.in.tum.de/~oheimb/

• Prev: JFP Special Issue on Haskell
• Next: IFIP TCS2000 preliminary program
• Index(es):
  • Main
  • Thread