Java Validation

Resources

Class notes on ESCJava

Paper by ESCJava authors

Formal methods and real programs

In OO design, focus on classes and objects

• Methods and messages are subordinate
   
• Collections of objects have state, which is the set of all active objects and the values of their variables at any moment of run time.
   
• Formal specifications P and Q are therefore logical expressions about each object’s state.

Tools for the formal design process

• Specifications : Java Modeling Language (JML) and ESC/Java (Extended Static Checker for Java)
   
• Design: Unified Modeling Language (UML, JML and ESC)
   
• Coding: Java, JML and ESC
   
• Verification: JML and ESC
   

What is JML? (www.jmlspecs.org)

History

• Emerged in early 2000s out of ESC/Java2

Goals

• Integration of formal methods throughout the software process
• Formal specification accessible to programmers
• Direct support for design by contract
• Integration with a real language (Java)

JML allows us to mix specifications directly with the Java code

• Preconditions
• Postconditions
• Loop invariants
• Class invariants

JML

Compiles assertions into Java byte-code to verify pre and postconditions, etc. (i.e. demonstrates that assertions hold at run-time).

Hoare triple

JML

{1 ≤ n}                                     P (precondition) int Factorial (int n) {   int f = 1;   int i = 1; { 1 ≤ i && i ≤ n && f == i! }    S (loop invariant)   while (i < n) {     i = i + 1;     f = f * i;   }   return f; } { f = n!}                                    Q (postcondition)

class Fact{ /*@            pre 1 <= n;            post \result==(\product int i; 1<=i && i<=n; i); @*/       int Factorial (int n) {            int f = 1;            int i = 1; /*@            loop_invariant                    i<=n && f==(\product int j; 1<=j && j<=i;  j); @*/             while (i < n) {                 i = i + 1;                 f = f * i;              }              return f;        } }

Language summary

JML expression (pragma)	Meaning
pre p;	p is a precondition for the call
post p;	p is a postcondition for the call
loop_invariant p;	p is a loop invariant
\result == e	e is the result returned by the call
(\product int x ; p(x); e(x) )	Õxєp(x) i.e., the product of e(x)
(\forall int x ; range(x); p(x) )	Universal quantifier over range(x) for quantifier expression p(x)
\old( v )	The value of v prior to method call or loop.

ESCjava

ESCjava has much the same syntax of JML and shares many of the same goals of enforcing formal specifications.

Difference is that ESCjava attempts to find specification errors in Java programs by static analysis of the program text while JML generates assertions that are tested at run-time.

ESCjava static analysis is similar to hand proofs of correctness.

Note that ESC does not have \product expression.

ESCjava and JML

• ESCjava analysis is static to validate program.
• JML generates Java byte-code with assertions to verify program at runtime.
• Complimentary parts of software development.
• Eclipse plug-ins available for both.

Exercise

1. Why is a proof of correctness preferred to testing?
2. Why, in practice, is testing done rather than a formal proof?
3. Give an example of a specification error in a function to calculate n!.
4. Give an example of a specification error in a function to sort an array.