Transcript Programming Languages Chapter 2: Syntax

Programming Languages
2nd edition
Tucker and Noonan
Chapter 18
Program Correctness
To treat programming scientifically, it must be possible to specify the
required properties of programs precisely. Formality is certainly
not an end in itself. The importance of formal specifications must
ultimately rest in their utility - in whether or not they are used to
improve the quality of software or to reduce the cost of
producing and maintaining software.
J. Horning
Copyright © 2006 The McGraw-Hill Companies, Inc.
Contents
18.1 Axiomatic Semantics
18.2 Formal Methods Tools: JML
18.2.1 JML Exception Handling
18.3 Correctness of Object-Oriented Programs
18.3.1 Design by Contract
18.3.2 The Class Invariant
18.3.3 Correctness of a Queue Application
18.3.4 Final Observations
18.4 Correctness of Functional Programs
Copyright © 2006 The McGraw-Hill Companies, Inc.
Review JML
JML Expression
Meaning
requires p;
ensures p;
signals (E e) p;
p is a precondition for the call
p is a postcondition for the call
when exception e is raised by the call, p is
a postcondition
loop_invariant p;
p is a loop invariant
invariant p;
p is a class invariant
\result == e;
e is the result returned by the call
\old v
the value of v at entry to the call
(\product int x ; p(x); e(x))
the product of e(x) for all x that satisfy p(x)
(\sum int x ; p(x); e(x)) the sum of e(x) for all x that satisfy p(x)
p ==> q
pq
Copyright © 2006 The McGraw-Hill Companies, Inc.
18.3.1 Design by Contract
Obligations
Benefits
Client
(caller)
Arguments for each
The call delivers correct
method/constructor call result, and the object keeps
must satisfy its requires its integrity
clause
Class
(object)
Result for each call must Called method/constructor
satisfy both its ensures doesn’t need extra code to
clause and INV
check argument validity
Note: Blame can be assigned if obligations aren’t met!
Copyright © 2006 The McGraw-Hill Companies, Inc.
The contract for a Queue class
O blig a tion s
C lien t
(call er)
C la ss
(o bj ect )
B en ef its
Ar gu m ents f o r ever y ca ll to
Q ueue (), enq u eue,
deq u eue, f ront,
is Em p ty, s iz e , an d
d isp lay
m ust s ati sfy its requ ire s
clause
E ver y ca ll to
Q ueue (), enq u eue,
deq u eue,, f ront,
is Em p ty, s iz e , an d
d isp lay
d eli ve rs a c orre ct re su lt,
and th e ob ject ke ep s its
in te gr ity
R es ult fro m ea ch cal l m ust
N o me th o d o r
con st ructo r n eed s ext ra
sati sfy b ot h its en s u res
clause a nd th e c lass in var ia n t code to c hec k a rg ume nt
n = = s iz e ()
v ali d it y
Copyright © 2006 The McGraw-Hill Companies, Inc.
18.3.2 The Class Invariant
A class C is formally specified if:
1. Every constructor and public method M in the class has
preconditions and postconditions, and
2. C has a special predicate called its class invariant INV
which, for every object o in C, argument x and call
o.M(x), must be true both before and after the call.
Note: During a call, INV may temporarily become false.
Why are we doing this???
i) Formal specifications provide a foundation for rigorous OO
system design (e.g., “design by contract”).
ii) They enable static and dynamic assertion checking of an
entire OO system.
iii) They enable formal correctness proof of an OO system.
Copyright © 2006 The McGraw-Hill Companies, Inc.
18.3.3 Correctness of a Queue Application
public class Queue {
private class Node { }
private Node first = null;
private Node last = null;
private int n = 0;
public void enqueue(Object v) { }
public Object dequeue( ) {}
public Object front() {}
public boolean isEmpty() {}
public int size() {}
public void display() {}
}
Copyright © 2006 The McGraw-Hill Companies, Inc.
public constructor
C = Queue()
“helper” class
state variables
help define INV
public
methods M
Adding Class-Level Specifications
JML model variables
/*@ public model Node H, T;
private represents H <- first;
private represents T <- last;
public invariant n == size();
@*/
private /*@ spec_public @*/ Node first = null;
private /*@ spec_public @*/ Node last = null;
private /*@ spec_public @*/ int n = 0;
class invariant INV
more JML
Notes: 1) JML model variables allow a specification to
distance itself from the class’s implementation details.
2) spec_public allows JML specifications to treat a Java
variable as public without forcing the code to do the same.
Copyright © 2006 The McGraw-Hill Companies, Inc.
Adding Method Specifications
/*@ ensures T.prior == \old(T) &&
H.prior == null && T.val.equals(v) ;
@*/
public void enqueue(Object v) {
last = new Node(v, last, null);
if (first == null)
first = last;
else (last.prior).next = last;
n = n+1;
}
Notes: 1) \old denotes the value of T at entry to enqueue.
2) The ensures clause specifies that enqueue adds
v to the tail T, and that the head H is not affected.
Copyright © 2006 The McGraw-Hill Companies, Inc.
What specifications for dequeue?
/*@
@*/
public Object dequeue( ) {
Object result = first.val;
first = first.next;
if (first != null)
first.prior = null ;
else last = null;
n = n-1;
return result;
}
Copyright © 2006 The McGraw-Hill Companies, Inc.
“Pure” methods
/*@ requires n > 0;
ensures \result == H.val && H == \old(H);
@*/
public /*@ pure @*/ Object front() {
return first.val;
}
Note: A method is pure if:
1) it has no non-local side effects, and
2) it is provably non-looping.
Copyright © 2006 The McGraw-Hill Companies, Inc.
Test driving the Queue class
public class QueueTest {
public static void main(String[] args) {
Queue q = new Queue();
int val;
int n = Integer.parseInt(args[0]);
for (int i=1; i <= n; i++)
q.enqueue(args[i]);
System.out.print("Queue contents = "); q.display();
System.out.println("Is Queue empty? " + q.isEmpty());
System.out.println("Queue size = " + q.size());
while (! q.isEmpty()) {
System.out.print(" dequeue " + q.dequeue());
System.out.print(" Queue contents = "); q.display();
}
System.out.println("Is Queue empty now? " + q.isEmpty());
}
}
Copyright © 2006 The McGraw-Hill Companies, Inc.
Contract test 1: normal run
% jmlrac QueueTest 5 1 2 3 4 5
Queue contents = last --> 5 4 3 2 1 <-- first
Is Queue empty? false
Queue size = 5
dequeue 1 Queue contents = last --> 5 4 3 2 <-- first
dequeue 2 Queue contents = last --> 5 4 3 <-- first
dequeue 3 Queue contents = last --> 5 4 <-- first
dequeue 4 Queue contents = last --> 5 <-- first
dequeue 5 Queue contents = last --> <-- first
Is Queue empty now? true
%
Copyright © 2006 The McGraw-Hill Companies, Inc.
Contract test 2: precondition violation
Queue contents = last --> 1 2 3 4 5 <-- first
…
dequeue 4 Queue contents = last --> 5 <-- first
dequeue 5 Queue contents = last --> <-- first
Exception in thread "main"
org.jmlspecs.jmlrac.runtime.JMLEntryPreconditionError: by method
Queue.dequeue regarding specifications at File
"../../home/allen/Desktop/workspace/myQueueTest/myqueuetest/
Queue.java", line 36, character 29 when
'this' is myqueuetest.Queue@b166b5
at myqueuetest.Queue.checkPre$dequeue$Queue(Queue.java:626)
at myqueuetest.Queue.dequeue(Queue.java:771)
at myqueuetest.QueueTest.main(QueueTest.java:16)
Note: blame is with the caller QueueTest, since a precondition
has been violated.
Copyright © 2006 The McGraw-Hill Companies, Inc.
Contract test 3: postcondition violation
Queue contents = last --> 5 4 3 2 1 <-- first
Is Queue empty? False
Exception in thread "main" org.jmlspecs.jmlrac.runtime.
JMLNormalPostconditionError:
by method Queue.dequeue regarding specifications
at File "../../home/allen/Desktop/workspace/
myQueueTest/myqueuetest/Queue.java",
line 37, character 52 when
'\old(H)' is myqueuetest.Queue$Node@b166b5
'\result' is 5
'this' is myqueuetest.Queue@cdfc9c
…
Note: blame is with the supplier Queue, since a postcondition has
been violated.
Copyright © 2006 The McGraw-Hill Companies, Inc.
Contract test 4: invariant error
% jmlrac QueueTest 5 1 2 3 4 5
Exception in thread "main"
org.jmlspecs.jmlrac.runtime.JMLInvariantError:
by method Queue.enqueue@post<File
"../../home/allen/Desktop/workspace/
myQueueTest/myqueuetest/Queue.java",
line 28, character 24> regarding
specifications at File
"../../home/allen/Desktop/workspace/myQueueTest/
myqueuetest/Queue.java",
line 22, character 38 …
Note: blame is again with the supplier Queue, since an invariant
has been violated.
Copyright © 2006 The McGraw-Hill Companies, Inc.
Class and System Correctness
So far, we have only done testing; what about formal verification?
1. A class C is (formally) correct if:
a. It is formally specified, and
b. For every object o and every constructor and public
method M in the class, the Hoare triple
{ P  INV } o.M ( x ) {Q  INV }
is valid for every argument x.
2.

A system is correct if all its classes are correct.
Copyright © 2006 The McGraw-Hill Companies, Inc.
E.g., Correctness of dequeue()
1.
2.
3.
4.
5.
6.
7.
/*@ requires n > 0;
ensures \result.equals(\old(H).val) && H == \old(H).next;
@*/
public Object dequeue( ) {
Object result = first.val;
first = first.next;
if (first != null)
first.prior = null ;
To prove:
{ P  INV } dequeue (){ Q  INV }
else last = null;
n = n-1;
where:
return result;
P n0
}
Q  \ result  \old ( first ).val  first  \old ( first ).next
INV  n  size ()
Note: We again use rules of inference and reason through the code,
just like we did with Factorial.

Copyright © 2006 The McGraw-Hill Companies, Inc.
A “loose” correctness proof for dequeue()
1. “Loose” because
a. We assume the validity of size(), and
b. We omit some details.
2. The assignments in dequeue(), together with P  INV ,
ensure the validity of Q  INV :
a. Steps 1 and 7 establish \result = \old(first).val
b. Steps 2-5 establish first = \old(first).next
c. Step 6 and our assumption establish
 n = size():
I.e., n =\old(n) -1
and size() = \old(size()) -1
So, n = size(), since \old(n) = \old(size())
Copyright © 2006 The McGraw-Hill Companies, Inc.
18.3.4 Final Observations
1. Formal verification:
a. is an enormous task for large programs.
b. only proves that specifications and code agree.
c. only proves partial correctness (assumes termination).
2. Tools exist for:
a. Statically checking certain run-time properties of Java
programs (ESC/Java2)
b. formally verifying Ada programs (Spark)
3. Tools are being developed to help with formal verification
of Java programs (Diacron, LOOP)
4. What is the cost/benefit of formal methods?
Copyright © 2006 The McGraw-Hill Companies, Inc.