Transcript int

Rigorous Software Development
CSCI-GA 3033-011
Instructor: Thomas Wies
Spring 2012
Lecture 8
Run-time vs. Static Checking
• Runtime Assertion Checking (RAC)
–
–
–
–
finds errors at run time,
tests for violation during execution,
can check most of the JML,
depends on appropriate test cases.
• (Extended) Static Checking (ESC)
–
–
–
–
–
finds errors at compile time,
proves that there is no violation
higher degree of confidence,
can check only parts of the JML,
does not require test cases.
ESC/Java 2
• Developed by the DEC Software Research Center (now HP
Research)
• Extended by David Cok and Joe Kiniry (Kind Software)
• Proves correctness of Java code wrt. JML specifications
• Is not sound: may approve an incorrect program
• Is not complete: may complain about a correct program
• Is useful to find many errors
• Works with Java 1.5
Homepage:
http://kindsoftware.com/products/opensource/ESCJava2
Download link:
ESCJava2.0.5
Importance of Specifications
• ESC/Java checks that each method behaves
correctly in all calling contexts admitted by the
specification.
• Programmer needs to provide method contracts
and invariants to reduce the number of alarms
produced by the tool.
• The tool emits three types of alarms:
– error: program is not well-formed (syntax/type error)
– warning: a likely error that might disappear when the
user provides a stronger specification
– caution: a property has not been checked
Absence of Runtime Exceptions
ESC checks that no undeclared runtime exceptions
occur.
• NullPointerException
• ClassCastException
• ArrayIndexOutOfBoundsException
• ArrayStoreException
• ArithmeticException
• NegativeArraySizeException
• other run-time exception, e.g., when calling
library functions.
ESC/Java and JML Specifications
• ESC/Java also checks JML specifications:
–
–
–
–
–
ensures clauses at end of a called method,
requires clauses before call of a method,
assert statements,
signals clauses,
invariants (loop invariants and class invariants).
• ESC/Java assumes that some specifications hold:
–
–
–
–
requires clauses at entry of a method,
ensures clauses after return of a called method,
assume statements,
invariants (loop invariants and class invariants).
ESC/Java 2 Demo
Consider the following code:
Object[] a;
void m(int i) {
a[i] = "Hello";
}
• Is a a null pointer? (NullPointerException)
• Is i non-negative? (ArrayIndexOutOfBoundsException)
• Is i smaller than the array length?
(ArrayIndexOutOfBoundsException)
• Is a an array of Object or String? (ArrayStoreException)
ESC/Java warns about these issues.
NullPointerException
public void put(Object o) {
int hash = o.hashCode();
...
}
ESC/Java reports: Possible null dereference
Solutions:
• Declare o as non_null.
• Add o != null to precondition.
• Add throws NullPointerException
or add signals (NullPointerException) o == null.
• Add Java code that handles null pointers:
int hash = (o == null ? 0 : o.hashCode());
ClassCastException
class Priority implements Comparable {
public int compareTo(Object other) {
Priority o = (Priority) other;
...
}
}
ESC/Java reports: Possible type cast error.
Solutions:
• Add throws ClassCastException or add
signals (ClassCastException) !(other instanceof Priority))
• Add Java code that handles differently typed objects:
if (!(other instanceof Priority))
return -other.compareTo(this)
Priority o = ...
ArrayIndexOutOfBoundsException
void write(/*@non_null@*/ byte[] what, int offset, int len) {
for (int i = 0; i < len; i++) {
write(what[offset + i]);
}
}
ESC/Java reports: Possible negative array index
Solution:
• Add offset >= 0 to pre-condition.
This results in Array index possibly too large.
• Add offset + len <= what.length.
• ESC/Java does not complain but there is still a problem.
If offset and len are very large numbers, then offset + len can be
negative. The code would throw an ArrayIndexOutOfBoundsException
at runtime.
• The correct pre-condition is:
/*@ requires offset >= 0 && offset + len >= offset &&
@
offset + len <= what.length;
@*/
ArrayStoreException
public class Stack {
/*@non_null@*/ Object[] elems;
int top;
/*@ invariant 0 <= top && top <= elems.length @*/
/*@ requires top < elems.length; @*/
void add(Object o) {
elems[top++] = o;
}
ESC/Java reports:
Type of right-hand side possibly not a subtype of array element type (ArrayStore).
Solutions:
• Add an invariant \typeof(elems) == \type(Object[]).
• Add a precondition \typeof(o) <: \elemtype(\typeof(elems)).
Java Types and JML
• \typeof gets the runtime type of an expression:
\typeof(obj) » obj.getClass()
• \elemtype gets the base type of an array type:
\elemtype(t1) » t1.getComponentType()
• \type gets the type representing the given Java type:
\type(Foo) » Foo.class
• <: means is sub-type of:
t1 <: t2 » t2.isAssignableFrom(t1)
ArithmeticException
class HashTable {
/*@non_null@*/ Bucket[] buckets;
void put(/*@non_null@*/ Object key, Object val) {
int hash = key.hashCode() % buckets.length;
...
}
ESC/Java reports: Possible division by zero
Solution:
• Add class invariant buckets.length > 0.
• Run ESC/Java again to check that this invariant holds.
It probably warns about a Possible negative array index.
Exceptions in Library Functions
class Bag {
/*@ non_null @*/ Object[] elems;
void sort() {
java.util.Arrays.sort(elems);
}
}
ESC/Java reports: Possible unexpected exception
• Look in escjava/specs/java/util/Arrays.refines-spec!
• Array.sort() has pre-condition:
elems[i] instanceof Comparable for all i.
• Solution: Add similar condition as class invariant.
Modular Checking
• ESC/Java checks each method in each class in
isolation.
• Each method body is transformed into
straight-line code with inlined specs, but with
all method calls and loops eliminated.
• Straight-line code is then transformed into
logical formulas that are given to an
automated theorem prover.
assume and assert
The basic specifications in ESC/Java are assume and
assert.
/*@ assume this.next != null; @*/
this.next.prev = this;
/*@ assert this.next.prev == this; @*/
• ESC/Java proves that if the assume statement holds in
the pre-state, the assert statement holds in the poststate.
• Such a triple of specification and code is called
Hoare triple.
Checking for Runtime Errors
To check for runtime errors ESC/Java automatically
inserts appropriate assert statements:
a[x] = "Hello";
becomes
/*@ assert a != null && x >= 0 && x < a.length &&
@
\typeof("Hello") <: \elemtype(\typeof(a));
@*/
a[x] = "Hello";
Inlining requires and ensures
The method specification is just translated into assume and
assert:
/*@ requires n > 0;
@ ensures \result == (int) Math.sqrt(n);
@*/
int m() {
body
return x;
}
becomes:
/*@ assume n > 0; @*/
body
/*@ assert x == (int) Math.sqrt(n); @*/
Eliminating Method Calls
And if method m is called, the roles of assume and
assert are interchanged:
...
y = m(x);
...
becomes:
...
/*@ assert x > 0; @*/
y = m_x; // m_x is a “fresh” variable
/*@ assume y == (int) Math.sqrt(x); @*/
...
Handling Loops
int a[] = new int[6];
for (int i = 0; i <= 6; i++) {
a[i] = i;
}
> escj -q Loop.java
0 warnings
> escj -Loop 7 -q Loop.java
Loop.java:5: Warning: Array index possibly too large
(IndexTooBig)
a[i] = i;
^
1 warning
> escj -LoopSafe -q Loop.java
Loop.java:5: Warning: Array index possibly too large
(IndexTooBig)
a[i] = i;
^
1 warning
Adding Loop Invariants
int a[] = new int[6];
for (int i = 0; i < 6; i++) a[i] = i;
> escj -LoopSafe -q Loop.java
Loop.java:6: Warning: Possible negative array index
(IndexNegative)
a[i] = i;
^
1 warning
Adding Loop Invariants
public void m() {
int a[] = new int[6];
//@ maintaining i >= 0;
for (int i = 0; i < 6; i++) a[i] = i;
}
> escj -LoopSafe -q Loop.java
0 warnings
Caution with assume
Never assume something that is not true,
otherwise ESC/Java will be able to prove
everything:
/*@nullable*/ Object o = null;
/*@ assume o != null; @*/
Object[] a = new String[-5];
a[-3] = new Integer(2);
> escj -q BadAssume.java
0 warnings
ESC/Java is not complete
ESC/Java can only do limited reasoning:
/*@ requires i == 5 && j== 3;
@ ensures \result == 15;
@*/
int m(int i, int j) {
return i*j;
}
Incomplete.java:7: Warning: Postcondition possibly not established (Post)
}
^
Associated declaration is “Incomplete.java", line 3, col 6:
@ ensures \result == 15;
Adding a good assumption can help eliminate such warnings, e.g.
int m(int i, int j) {
/*@ assume 15 == 5 * 3; @*/
return i*j;
}
But this is dangerous since assume statements are not checked.
Class Invariants
• Class invariants are properties that must hold at
the entry and exit point of every method
• They often express properties about the
consistency of the internal representation of an
object.
• They are typically transparent to clients of an
object.
• They are sometimes also called object invariants
or instance invariants.
The Problem with Class Invariants
There are some problems with class invariants:
• Ownership: invariants can depend on fields of
other objects.
– For example, the invariant of List accesses Node
fields.
• Callback: invariants can be temporarily violated.
– While the invariant is violated, we call a different
method that calls back to the same object.
• Atomicity: invariants can be temporarily violated.
– While the invariant is violated, another thread
accesses object.
The Problem with Class Invariants
public class SomeClass {
public class OtherClass {
/*@ invariant inv; @*/
public void caller(SomeClass o)
/*@ requires P;
{
@ ensures Q;
...some other code...
@*/
//@ assert(P);
public void doSomething() {
o.doSomething();
//@ assume(P);
//@ assume(Q);
//@ assume(inv);
}
...code of doSomething... }
//@ assert(Q);
//@ assert(inv);
}
}
• ESC/Java checks the highlighted assumes and asserts.
• This is unsound!
Invariants May Depend on Other Objects
Consider a doubly linked list:
class Node {
Node prev, next;
/*@ invariant this.prev.next == this &&
this.next.prev == this; @*/
}
class List {
private Node first;
public void add() {
Node newnode = new Node();
newnode.prev = first.prev;
newnode.next = first;
first.prev.next = newnode;
first.prev = newnode;
}
}
The invariant of this depends on the fields of this.next and
this.prev. Moreover the List.add function changes the
fields of the invariants of Node.
List Example
First observation: the invariant should be put into the List class:
class Node { Node prev, next; }
class List {
private Node first;
/*@ private ghost JMLObjectSet nodes; @*/
/*@ invariant (\forall Node n; nodes.has(n);
n.prev.next == n && n.next.prev == n); @*/
public void add() {
Node newnode = new Node();
newnode.prev = first.prev;
newnode.next = first;
first.prev.next = newnode;
first.prev = newnode;
//@ set nodes = nodes.insert(newnode);
}
}
List Example
Second observation: Node objects much not be shared between to
different lists.
class Node {
/*@ ghost Object owner; @*/
Node prev, next;
}
class List {
private Node first;
/*@ private ghost JMLObjectSet nodes; @*/
/*@ invariant (\forall Node n; nodes.has(n); n.prev.next == n &&
n.next.prev == n && n.owner == this); @*/
public void add() {
Node newnode = new Node();
//@ set newnode.owner = this;
newnode.prev = first.prev;
newnode.next = first;
first.prev.next = newnode;
first.prev = newnode;
//@ set nodes = nodes.insert(newnode);
}
List Example
Third observation: One may only change the owned fields.
class Node {
/*@ ghost Object owner; @*/
Node prev, next;
}
class List {
private Node first;
/*@ private ghost JMLObjectSet nodes; @*/
/*@ invariant (\forall Node n; nodes.has(n); n.prev.next == n &&
n.next.prev == n && n.owner == this); @*/
public void add() {
Node newnode = new Node();
//@ set newnode.owner = this;
newnode.prev = first.prev;
newnode.next = first;
//@ assert(first.prev.owner == this)
first.prev.next = newnode;
//@ assert(first.owner == this)
first.prev = newnode;
//@ set nodes = nodes.insert(newnode);
}
The Owner-As-Modifier Property
JML supports a type system for checking the owner-as-modifier
property, when invoked as
jmlc --universes.
The underlying type system is called Universes:
• The class Object has a ghost field owner.
• Fields can be declared as rep, peer, readonly.
– rep Object x adds an implicit invariant (or requires)
x.owner = this.
– peer Object x adds an implicit invariant (or requires)
x.owner = this.owner.
– readonly Object x does not restrict owner, but does not
allow modifications of x.
• The new operation supports rep and peer:
– new /*@rep@*/Node() sets owner field of new node to this.
– new /*@peer@*/Node() sets owner field of new node to
this.owner.
List with Universes Type System
class Node { /*@ peer @*/ Node prev, next; }
class List {
private /*@ rep @*/ Node first;
/*@ private ghost JMLObjectSet nodes; @*/
/*@ invariant (\forall Node n; nodes.has(n);
n.prev.next == n && n.next.prev == n &&
n.owner == this); @*/
public void add() {
Node newnode = new /*@ rep @*/ Node();
newnode.prev = first.prev;
newnode.next = first;
first.prev.next = newnode;
first.prev = newnode;
//@ set nodes = nodes.insert(newnode);
}
}
The Universes Type System
A simple type system can check most issues
related to ownership:
• rep T can be assigned without cast to rep T
and readonly T.
• peer T can be assigned without cast to peer
T and readonly T.
• readonly T can be assigned without cast to
readonly T.
The Universes Type System
One needs to distinguish between the type of a
field peer Node prev and the type of a field
expression rep Node first.prev.
• If obj is a peer type and fld is a peer T field
then obj.fld has type peer T.
• If obj is a rep type and fld is a peer T field
then obj.fld has type rep T.
• If obj = this and fld is a rep T field then
this.fld has type rep T.
• In all other cases obj.fld has type
readonly T.
readonly References
To prevent changing readonly references, the
following restrictions apply:
• If obj has type readonly T, then
– obj.fld = expr is illegal.
– obj.method(...) is only allowed if method is a
pure method.
• It is allowed to cast readonly T references to
rep T or peer T:
– (rep T) expr asserts that expr.owner == this.
– (peer T) expr asserts that
expr.owner == this.owner.
Modification only by Owner
All write accesses to a field of an object obj are
• in a method of the owner of obj or
• in a method of an object having the same
owner as the object that was invoked (directly
or indirectly) by the owner of obj.
Invariants that only depend on fields of owned
objects can only be invalidated by the owner or
methods that the owner invokes.