Transcript Slides - Resource Analysis

The Java Modeling Language
JML
Erik Poll
Digital Security
Radboud University Nijmegen
Topics
• What properties can you specify in JML?
• What properties you want to specify? And why?
– what kind of properties
– at what level of detail
• Where do these properties come from?
– ‘external’ system requirements
– ‘internal’ design decisions
JML
• formal specification language for sequential Java
by Gary Leavens et. al.
– to specify behaviour of Java classes & interfaces
– to record detailed design decisions
by adding assertions aka annotations to Java source code in
Design-By-Contract style, using eg.
– pre/postconditions
– object invariants
– loop invariants
– lots of other stuff
• Design goal:
JML is meant to be usable by any Java programmer
Lots of info on http://www.jmlspecs.org
to make JML easy to use
• JML annotations added as special Java comments, between
/*@ .. @*/ or after //@
• JML specs can be in .java files, or in separate .jml files
• Properties written in Java syntax, extended with some
operators
\old( ), \result, \forall, \exists, ==> , ..
and some keywords
requires, ensures, invariant, ....
JML example
public class ePurse{
private int balance;
//@ invariant 0 <= balance && balance < 500;
//@ requires amount >= 0;
//@ ensures balance <= \old(balance);
public void debit(int amount) {
if (amount > balance) {
throw (new BankException("No way"));}
balance = balance – amount;
}
What can you do with this?
• documentation/specification
– record detailed design decisions & document assumptions
(and hence obligations!)
– precise, unambiguous documentation
• parsed & type checked
• use tools for
– runtime assertion checking
• ie. testing code
– compile time (static) analyses
• up to full formal program verification
preconditions assign responsibilities
//@ requires amount >= 0;
public debit(int amount)
{ ... }
vs
//@ requires true;
public debit(int amount)
{ if (amount < 0) return;
... }
Preconditions clearly assign responsibility on caller
• and may remove the need for defensive coding
Dually, postconditions clearly assign responsibility on callee
LOTS of freedom in specifying
JML specs can be as strong (aka detailed) or weak as you want
Eg for debit(int amount)
//@ ensures balance == \old(balance)-amount;
or
//@ ensures balance <= \old(balance);
or
//@ ensures true;
Even last spec is stronger than you may think!
LOTS of freedom in specifying
JML spec can express implementation decision
//@ invariant f != null;
or document a more interesting, deeper property
//@ invariant child.parent == this;
What can you specify in JML?
exceptional postconditions: signals
/*@ requires amount >= 0;
@ ensures balance <= \old(balance);
@ signals (BankException) balance == \old(balance);
@*/
public debit(int amount) throws BankException {
if (amount > balance) {
throw (new BankException("No way"));}
balance = balance – amount;
}
Often specs (should) concentrate on ruling out exceptional
behaviour
ruling out exceptions
/*@ normal_behavior
@ requires amount >= 0 && amount <= balance;
@ ensures balance <= \old(balance);
@*/
public debit(int amount) throws BankException{
if (amount > balance) {
throw (new BankException("No way"));}
balance = balance – amount;
}
Or omit “throws BankException”
In JML, unlike Java, runtime exceptions not explicitly declared are
not allowed to be thrown.
loop_invariants and decreasing clauses
/*@ loop_invariant 0 <= i && i < a.length &
(\forall int j; 0<= j & j < i;
a[i] != null );
decreasing
a.length-i;
@*/
while (a[i] != null) {...}
non_null
• Lots of invariants and preconditions are about references
not being null, eg
int[] a; //@ invariant a != null;
• Therefore there is a shorthand
/*@ non_null @*/ int[] a;
• But, as most references are non-null, JML adopted this as
default. So only nullable fields, arguments and return types
need to be annotated, eg
/*@ nullable @*/ int[] b;
• You can also use JSR308 Java tags for this
@Nullable int[] b;
pure
Methods without side-effects that are guaranteed to terminate can
be declared as pure
/*@ pure @*/ int getBalance (){
return balance;
};
Pure methods can be used in JML annotations
//@ requires amount < getBalance();
public debit (int amount)
resource usage
Syntax for specifying resource usage
/*@ measured_by len;
// max recursion depth
@ working_space (len*4); // max heap space used
@ duration len*24;
// max execution time
@ ensures \fresh(\result); // freshly allocated
@*/
public List(int len) {...
}
Lots on JML syntax, much of it not supported by specific tools
How and what to specify?
Where do properties come from?
• JML does not provide any methodology or development
process for coming up with annotations
• JML specs can
1. capture system requirements
2. document detailed decisions made in design or
implementation
• making some implicit requirement or guarantee explicit
3. document requirements or guarantees that follow from
others
• a single invariant someField != null may lead to many
preconditions about arguments not being null, in turn requiring many
postconditions about results not being null,etc,etc
Example specs expressing “external” requirements
int balance;
//@ invariant 0 <= balance && balance < 500;
//@ ensures \result >= 0;
public /*@ pure @*/ int getBalance ()
These specs might be traced back to an important functional (or
security) requirements for a banking application
– assuming that getBalance is part of the public interface of
the overall system
Example specs capturing “internal” design decisions
private int length;
//@ invariant 0 <= len && len < values.length;
private int[] values;
//@ invariant values != null;
These invariants are probably internal design decisions and not
mentioned anywhere in the system requirements
How do you start specifying?
Useful bottom-line specs to start specifying
specify that methods do not throw unwanted runtime
exceptions
or
•
such specs are simple, easy to understand, obviously correct, and
capture important (safety) requirement
•
satisfying such a bottom-line specs may rely on many (implicit!)
assumptions that can be made explicit in preconditions and
invariants
How do you start specifying?
Another way to start specifying
for almost every field, there is an (implicit) invariant
– eg integer fields being non-negative,
arrays having some minimal/maximal/exact
length,
or
reference fields being non-null, etc.
Again, satisfying these specs may rely on many others
– eg lots of preconditions to prevent violating invariant (or
defensive coding)
Added value of specs?
int i;
//@ invariant 0 <= i;
//@ ensures i = (\old(i)<20) ? i :(\old(i)+1)*24;
public void increase(){
if i < 20 {i = (i + 1)*24};
}
Added value of specs?
• Some specs closely mirror program code
– eg, a postcondition expressing a detailed functional spec
may closely resemble the program code
• Other specs document properties that are nowhere to be
found in the program code (or, at best, very implicitly)
– typical example: invariants & preconditions
Latter are provbably more “interesting” than former
When to stop specifying
The challenge of using JML: choosing
• which properties to verify
• up to which level of detail
• and using which tools
so that JML specs are cost effective
cost
more detailed specs,
(hence?) higher assurance
What can you specify in JML?
(continued)
assignable (aka modifies)
For non-pure methods, frame properties can be specified using
assignable clauses, eg
/*@
requires amount >= 0;
assignable balance;
ensures balance == \old(balance) – amount;
@*/
void debit()
says debit is only allowed to modify the balance field
• NB this does not follow from the postcondition
• Assignable clauses are needed for modular verification
•
Fields can be grouped in Datagroups, so that spec does not have to
list concrete fields
model state
interface Connection{
//@ model boolean opened; // spec-only field
//@ ensures !opened;
public Connection(...);
//@ requires !opened;
//@ ensures
opened;
public void open ();
//@ requires opened;
//@ ensures !opened;
public void close ();
questions?
tools, ...
tool support: runtime assertion checking
• annotations provide the test oracle:
– any annotation violation is an error,
except if it is the initial precondition
• Pros
– Lots of tests for free
– Complicated test code for free, eg for
signals (Exception) balance ==\old(balance);
– More precise feedback about root causes
• eg "Invariant X violated in line 200" after 10 sec instead of
"Nullpointer exception in line 600" after 100 sec
tool support: compile time checking
• extended static checking
automated checking of simple specs
– ESC/Java(2)
• formal program verification tools
interactive checking of arbitrarily complex specs
– KeY, Krakatoa, Freeboogie, JMLDirectVCGen....
There is a trade-off between usability & qualifability.
In practice, each tool support its own subset of JML.
testing vs verification
•
verification gives complete coverage
–
all paths, all possible inputs
•
if testing fails, you get a counterexample (trace);
if verification fails, you typically don't....
•
verification can be done before code is complete
•
verification requires many more specs
–
as verification is done on a per method basis
–
incl API specs