EscJava

ExtendedStaticChecking for JavaLanguage

See

http://secure.ucd.ie/products/opensource/ESCJava2/

http://secure.ucd.ie/products/opensource/ESCJava2/ESCTools/docs/ESCJAVA-UsersManual.html

For an idea how this works see ProofAnnotationsForBubbleSort.

There seem to be versions for Modula 3 and Haskell now:

• http://lambda-the-ultimate.org/node/1689 -> http://www.cl.cam.ac.uk/~nx200/research/escH-hw.ps

For a general review see http://radu.ucd.ie/hp/papers/phd.pdf

---

CategoryLanguageTyping