JML Tutorial - Reasoning about recursive functions and data structures (model method version)
Last Modified:
This example extends the lesson about recursion with the same singly-linked list example but modeled with model methods instead of model fields.
// ## openjml --esc --progress --timeout=300 ListMM.java
/** This file contains a worked (specified and verified) example of a singly-linked list using JML and OpenJML.
* It is intended to illustrate techniques that can be used for other simple recursive data structures.
* This example uses model methods.
*
* A list of values of type T is an instance of the public class ListMM<T>. The actual links are instances of the non-public
* nested class Node<T>; both classes inherit from Link<T>, which contains common functionality. The linked-list is formed
* by the typical chain of 'next' field references, with a null reference at the end of the list. The starting point, the List
* object, is not a part of the abstract list.
*
*/
/** Parent class for ListMM and Node containing the 'next' field and common functionality */
class Link<T> {
//@ public model JMLDataGroup ownerFields;
//@ ghost helper nullable public ListMM<T> owner; //@ in ownerFields; maps next.ownerFields \into ownerFields;
// True if my owner is the argument and all nodes after me have the argument as their owners.
//@ public normal_behavior
//@ reads this.owner, this.next.ownerFields, this.nextFields;
//@ ensures \result == (this.owner == owner && (next != null ==> next.allMine(owner)));
//@ model pure helper public boolean allMine(ListMM<T> owner);
//@ public normal_behavior
//@ reads next, next.next, next.nextFields, next.value, next.valueFields;
//@ ensures \result == (next == null ? seq.<T>empty() : next.values().prepend(next.value));
//@ pure helper
//@ model public seq<T> values(); // sequence of values after the current Link, not including the current Link
//@ public normal_behavior
//@ reads next, next.next, next.nextFields;
//@ ensures \result == (next == null ? seq.<Link<T>>empty() : next.links().prepend(next));
//@ pure helper
//@ model public seq<Link<T>> links(); // sequence of nodes after the current Link, not including the current Link
//@ public normal_behavior
//@ reads next, next.next, next.nextFields; // FIXME - does not work as nextFields
//@ ensures \result == ((next == null) ? 0 : 1 + next.size());
//@ ensures \result >= 0;
//@ pure helper
//@ model public \bigint size();
//@ public model JMLDataGroup nextFields;
//@ public model JMLDataGroup valueFields;
//@ public invariant this.owner != null && allMine(this.owner);
//@ public invariant values().size() == this.size();
//@ public invariant links().size() == this.size();
//@ public invariant !links().contains(this);
//@ nullable spec_public
protected ListMM.Node<T> next; //@ in valueFields, nextFields, ownerFields;
//@ maps next.valueFields \into valueFields;
//@ maps next.nextFields \into nextFields;
//@ maps next.ownerFields \into ownerFields;
//@ protected normal_behavior
//@ pure helper
protected Link() {
}
/** Returns the nth value in the list */
//@ public normal_behavior
//@ requires 0 <= n < this.values().size();
//@ reads valueFields, nextFields;
//@ ensures \result == values()[n];
//@ pure
public T value(int n) {
if (n == 0) {
return next.value();
} else {
//@ assert next.values() == this.values().tail(1);
return next.value(n-1);
}
}
/** Removes the nth value from the list */
//@ public normal_behavior
//@ requires 0 <= n < this.size();
//@ old \bigint oldsize = this.size();
//@ old seq<T> oldvalues = this.values();
//@ old seq<Link<T>> oldlinks = this.links();
//@ assignable next, nextFields, valueFields, ownerFields;
//@ ensures this.size() == oldsize - 1;
//@ ensures this.values().size == oldvalues.size - 1;
//@ ensures this.links().size == oldlinks.size - 1;
//@ ensures n==0 ==> this.values() == oldvalues.tail(1);
public void remove(int n) {
//@ assert this.next != null;
//@ ghost \bigint newsize = this.size() - 1;
//@ ghost seq<T> oldvalues = this.values();
//@ assert this.values().size() == oldvalues.size();
//@ assert this.owner != null && allMine(this.owner);
//@ assert this.next.allMine(this.next.owner);
//@ assert this.next.next != null ==> this.next.next.allMine(this.next.next.owner);
if (n == 0) {
//@ assert this.next.size() == newsize;
//@ assert this.next.next != null ==> this.next.next.size() == newsize - 1;
//@ assert this.next.allMine(this.next.owner);
//@ assert this.next.next != null ==> this.next.next.allMine(this.next.next.owner);
//@ assert this.next.values().size == newsize;
//@ assert this.next.values() == oldvalues.tail(1);
//@ assert this.next.next != null ==> this.next.next.values().size == newsize - 1;
//@ assert this.next.links().size == newsize;
//@ assert this.next.next != null ==> this.next.next.links().size == newsize - 1;
this.next = this.next.next;
//@ assert this.next != null ==> this.next.size() == newsize - 1;
//@ assert this.size() == newsize;
//@ assert this.next != null ==> this.next.allMine(this.next.owner);
//@ assert this.allMine(this.owner);
//@ assert this.next != null ==> this.next.values().size == newsize - 1;
//@ assert this.values().size == newsize;
//@ assert this.next != null ==> this.next.links().size == newsize - 1;
//@ assert this.links().size == newsize;
//@ assert this.values() == oldvalues.tail(1);
} else {
//@ ghost \bigint poldsize = this.next.size();
//@ assert this.next.owner != null && this.next.allMine(this.next.owner);
//@ assert this.next.values().size() == poldsize;
//@ assert this.next.links().size() == poldsize;
//@ reachable;
this.next.remove(n-1);
//@ reachable;
//@ assert this.next.owner != null && this.next.allMine(this.next.owner);
//@ assert this.next.values().size() == poldsize - 1;
//@ assert this.next.links().size() == poldsize - 1;
//@ assert this.owner == this.next.owner;
//@ assert this.next.allMine(this.owner);
//@ assert this.values().size() == poldsize;
//@ assert this.links().size() == poldsize;
//@ reachable;
}
//@ assert this.size() == newsize;
//@ assert this.allMine(this.owner);
//@ assert this.values().size == newsize;
//@ assert this.links().size == newsize;
//@ assert n==0 ==> this.values() == oldvalues.tail(1);
}
}
public class ListMM<T> extends Link<T> {
//@ public invariant this.owner == this;
/** Creates an empty list -- just an anchor node with null 'next' field */
//@ public normal_behavior
//@ ensures \result.values() == seq.<TT>empty();
//@ ensures \result.size() == 0;
//@ ensures \result.links() == seq.<Link<TT>>empty();
//@ ensures \result.next == null;
//@ ensures \result.owner == \result;
//@ pure
public static <TT> ListMM<TT> empty() {
return new ListMM<TT>();
}
//@ private normal_behavior
//@ ensures this.next == null;
//@ ensures this.owner == this;
//@ pure
private ListMM() {
this.next = null;
//@ set this.owner = this;
}
/** Pushes a new value onto the front of the list */
//@ public normal_behavior
//@ old \bigint oldsize = this.size();
//@ old seq<T> oldvalues = this.values();
//@ old seq<Link<T>> oldlinks = this.links();
//@ assignable next, valueFields, nextFields, ownerFields;
//@ ensures \fresh(this.next);
//@ ensures this.next.value == t;
//@ ensures this.next.next == \old(this.next);
//@ ensures this.size() == oldsize + 1;
//@ ensures this.values()== oldvalues.prepend(t);
//@ ensures this.links() == oldlinks.prepend(this.next);
public void push(T t) {
//@ ghost var oldvalues = this.values();
//@ ghost var oldlinks = this.links();
//@ ghost \bigint nn = (this.next == null ? -1 : this.next.size());
//@ assert allMine(this);
//@ assert this.next != null ==> this.next.allMine(this);
Node<T> v = new Node<T>(t, next);
//@ assert oldvalues == this.values();
//@ assert v.values() == oldvalues;
//@ assert v.size() == this.size();
//@ assert v.size() == \old(this.size());
//@ assert this.links() == oldlinks;
//@ assert v.links() == oldlinks;
//@ set v.owner = this;
//@ assert oldvalues == this.values();
//@ assert v.values() == oldvalues;
//@ assert this.links() == oldlinks;
//@ assert v.links() == oldlinks;
//@ assert v.size() == this.size();
//@ assert v.size() == \old(this.size());
//@ assert (v.owner == this && (v.next != null ==> v.next.allMine(v.owner)));
//@ assert v.allMine(this);
this.next = v;
//@ assert v.size() == \old(this.size());
//@ assert v.values() == oldvalues;
//@ assert this.values() == oldvalues.prepend(t);
//@ assert this.next != null ==> this.next.allMine(owner);
//@ assert this.allMine(this);
//@ assert v.links() == oldlinks;
//@ assert this.links() == oldlinks.prepend(v);
}
/** Removes the first value from the list */
//@ public normal_behavior
//@ requires this.size() > 0;
//@ old \bigint oldsize = this.size();
//@ old seq<T> oldvalues = this.values();
//@ assignable next, nextFields, valueFields, ownerFields;
//@ ensures this.size() == oldsize - 1;
//@ ensures this.values() == oldvalues.tail(1);
//@ ensures next == \old(next.next);
public void pop() {
//@ assert this.owner == this && this.allMine(this.owner);
//@ assert this.next.owner == this && this.next.allMine(this.owner);
//@ assert this.next.next != null ==> this.next.next.allMine(this.next.owner);
//@ assert this.next != null;
//@ assert this.values().size == this.size();
//@ assert this.next.values().size == this.next.size();
//@ assert this.next.next != null ==> this.next.next.values().size == this.next.next.size();
//@ assert next.links().size() == this.next.size();
//@ assert this.next.next != null ==> this.next.next.links().size == this.next.next.size();
//@ ghost seq<T> oldvalues = this.values();
//@ ghost seq<T> oldnvalues = this.next.values();
//@ assert oldnvalues == oldvalues.tail(1);
//@ ghost seq<Link<T>> oldlinks = this.links();
//@ ghost seq<Link<T>> newlinks = this.next.links();
//@ assert newlinks == oldlinks.tail(1);
this.next = this.next.next;
//@ assert this.size() == (this.next == null ? 0 : this.next.size() + 1);
//@ assert this.size() == \old(this.size()) - 1;
//@ assert this.next != null ==> this.next.values().size == this.next.size();
//@ assert this.next != null ==> this.next.links().size == this.next.size();
//@ assert this.values() == oldnvalues;
//@ assert this.values() == oldvalues.tail(1);
//@ assert this.links() == newlinks;
//@ assert this.links() == oldlinks.tail(1);
//@ assert this.allMine(this.owner) <==> (this.owner == owner && (this.next != null ==> this.next.allMine(this.owner)));
//@ assert this.allMine(this.owner);
}
static class Node<T> extends Link<T> {
/** Constructs a new link with given value and next field; for internal use only */
//@ private normal_behavior
//@ ensures this.next == next;
//@ ensures this.value == value;
//@ pure helper
private Node(T value, /*@ helper nullable */ Node<T> next) {
this.value = value;
this.next = next;
}
//@ spec_public
private T value; //@ in valueFields; maps next.valueFields \into valueFields;
/** Returns the value from this link */
//@ public normal_behavior
//@ reads value;
//@ ensures \result == value;
//@ pure helper
public T value() {
return value;
}
}
}
class Test {
/** properties of an empty list */
public static <Y> void testEmpty(Y y) {
var in = ListMM.<Y>empty();
//@ assert in.size() == 0;
//@ assert in.values().size() == 0;
//@ assert in.values() == seq.<Y>empty();
}
/** pushing a value and then retrieving it */
public static <Y> void testPushValue(ListMM<Y> in, Y y, Y yy) {
in.push(y);
//@ reachable;
//@ assert in.value(0) == y;
in.push(yy);
//@ reachable;
//@ assert in.value(1) == y;
//@ assert in.value(0) == yy;
}
/** pushing a value and then retrieving it */
//@ requires in.size() >= 2;
public static <Y> void testPopValue(ListMM<Y> in) {
Y y = in.value(1);
in.pop();
//@ reachable;
Y yy = in.value(0);
//@ assert y == yy;
}
/** pushing and popping leaves the list unchanged */
public static <Y> void testPushPop(ListMM<Y> in, Y y) {
in.push(y);
//@ reachable;
//@ assert in.size() == \old(in.size()) + 1;
//@ assert in.values() != \old(in.values());
in.pop();
//@ reachable;
//@ assert in.size() == \old(in.size());
//@ assert in.values() == \old(in.values());
}
/** pushing and removing the zeroth element leaves the list unchanged */
public static <Y> void testPushRemove(ListMM<Y> in, Y y) {
in.push(y);
//@ reachable;
//@ assert in.size() == \old(in.size()) + 1;
//@ assert in.values() != \old(in.values());
in.remove(0);
//@ reachable;
//@ assert in.size() == \old(in.size());
//@ assert in.values() == \old(in.values());
}
/** pushing a value on one list does not change the other */
//@ requires in != other;
//@ requires in.values() == other.values();
public static <Y> void testNI1(Y y, ListMM<Y> in, ListMM<Y> other) {
in.push(y);
//@ reachable;
//@ assert in.values().tail(1) == other.values();
}
/** popping a value from one list does not change the other */
//@ requires in != other;
//@ requires in.values() == other.values();
//@ requires in.size() > 0;
public static <Y> void testNI2(ListMM<Y> in, ListMM<Y> other) {
//@ assert in.size() == other.size();
//@ ghost seq<Y> oldvalues = in.values();
in.pop();
//@ reachable;
//@ assert oldvalues.tail(1) == in.values();
//@ assert in.values() == other.values().tail(1);
}
/** removing a value (other than the 0th) from one list might change the other,
* except when the owner invariant is used */
//@ requires in != other;
//@ requires in.values() == other.values();
//@ requires in.size() > 1;
public static <Y> void testNI3(ListMM<Y> in, ListMM<Y> other) {
//@ ghost seq<Y> oldvalues = in.values();
in.remove(1);
//@ reachable;
//@ assert oldvalues.size - 1 == in.size();
//@ assert other.values().size() - 1 == in.size(); // Should not be provable without the owner invariant
}
/** two different lists may have the same first element, except when the owner invariant is used */
//@ requires in != other;
//@ requires in.size() > 0;
//@ requires other.size() > 0;
public static <Y> void testNI4(ListMM<Y> in, ListMM<Y> other) {
//@ assert in.next.owner == in;
//@ assert other.next.owner == other;
//@ assert in.next != other.next; // Should not be provable without the owner invariant
}
/** using rep-exposure to change a value still does not change the other list if the owner invariant is used */
//@ requires in != other;
//@ requires in.values() == other.values();
//@ requires in.size() > 1;
//@ requires in.next.value != y;
/*@ model public static <Y> void testNI5(ListMM<Y> in, ListMM<Y> other, Y y) {
//@ assert in.values().size() > 1;
reachable;
ghost \bigint n = in.size();
assert in.values().size() == other.values().size();
assert in.size() == other.size();
assert in.size() == n;
reachable;
var nvalues = in.next.values();
in.next.value = y;
//@ assert in.next.values() == nvalues;
//@ assert in.values() == nvalues.prepend(y);
//@ assert in.values().size() > 1;
reachable;
assert in.size() == n;
reachable;
assert in.size() == other.size();
reachable;
assert in.values() != other.values(); // Should not be provable without the owner invariant
reachable;
assert in.values().tail(1) == other.values().tail(1);
reachable;
}
@*/
}