ESCJava2

TOC

Explanation

WikiInclude(ESCJava2Explanation)

Limitations

JML Keywords

ESC/Java2 does not recognise the following JML keywords

• \same
• \only_assigned
• nullable (within definition of a quantified variable)
• \pre
• when
• atomic
• independent
• locks
• monitors_for
• thread_safe

Java Specifications

ESC/Java2 uses JML specifications for the Java 1.4 JDK and for JavaCard 2.1. It will report inconsistencies when a Java 1.5 or Java 6 JDK is used.

Java 1.5 source

ESC/Java2 will check Java source code up to Java 1.4 and bytecode up to 1.5, but relies on the JML specifications for JDK 1.4.

Milestones and Tickets

• See [/query?status=new&status=assigned&status=reopened&component=ESC/Java2&order=priority tickets assigned to ESC/Java2].

Update Site for Eclipse Plugin

• The most recent version of the ESC/Java2 plugin is 2.0.14.

Example

WikiInclude(ESCJava2Example)

News and Status

WikiInclude(ESCJava2News)

Releases

WikiInclude(ESCJava2Releases)

Recent Changes

ChangeLog(src/escjava/trunk/ESCTools,3)

Owners

Dependencies and Subcomponents

ESC/Java2 depends on

• Javafe
• Simplify

Version: 14 Time: Tue May 5 18:54:08 2009 Author: dcochran (dcochran) IP: 78.152.239.227