|
Jean-Baptiste Tristan & K. Rustan M. Leino |
Verifying objects is different from code
So far, an invariant was always attached to a single function of statement
In an object, the invariant is shared by all methods in the class
The invariant might need to be framed using this
class B {
var x: nat
predicate Invariant()
reads this
{
x % 2 == 0
}
}constructor
class B {
// ...
constructor(x: nat)
requires x % 2 == 0
ensures Invariant()
{
this.x := x;
}
}Methods might also need to be framed
Methods/functions that read the object usually requires the invariant as a precondition
Methods/functions that modify the object must ensure the invariant as a postcondition
class B {
// ...
method Add(y: nat)
requires Invariant()
modifies this
ensures Invariant()
{
this.x := this.x + 2 * y;
}
}Some functions/methods read from the object
Typically, they ensures some postcondition
The invariant must be strong enough for the postcondition to hold
class B {
// ...
function Get(): nat
requires Invariant()
reads this
ensures Get() % 2 == 0
{
x
}
}Note that so far it would be fine for Add not to ensure the invariant
What would go wrong?
Function precondition might not hold when you use the object
class B {
// ..., but without postcondition of Add
}
method Client() {
var b: B := new B(2);
b.Add(3);
var c: nat := b.Get(); // Error
}As long as an object doesn't change what other objects in contains, the framing is static and simple
If an object uses another object, you must have some way to refer to its frame
Objects can define a ghost constant, usually called Repr (for representation),
to denote the set of contained objects
class D {
var x: nat
ghost const Repr: set<object> := {this}
}
class E {
method M(a: D)
modifies a.Repr
{
a.x := 4;
}
}Here again, ghost state is very useful
It can be used to relate the object to a purely functional implementation
It can be used to carry information about the past of the object
For example, to keep track of accesses to a storage
datatype Entry<T> = Entry(key: nat, value: T)
class Storage<T> {
ghost var log: seq<Entry<T>>
}Let's grow the API, strengthening the invariant as we go
class LL<T> {
const value: T
var next: LL?<T>
constructor(value: T)
ensures this.value == value
ensures this.next == null
{
this.value := value;
next := null;
}
}Cons creates a new cell and attaches to its tail
class LL<T> ... {
method Cons(v: T) returns (l: LL<T>) {
l := new LL(v);
l.next := this;
}
}Head and Tail can be defined as functions
class LL<T> ... {
function Head(): T {
value
}
function Tail(): LL<T>
requires next != null
reads this
{
next
}
}Length is problematic
We need to ensure that the function terminates
Intuitively we know why it does:
We intend for the LL not to be cyclic
We will need to explicitate our intentions in the invariant
class LL<T> ... {
function Length(): nat
reads this
{
1 + if next == null then 0 else next.Length() // Error: might not terminate
}
}We need to reason about the set of objects composing the LL
We can use a ghost set dynamic frame
We can state that a cell is not in the representation of its successor
This implies the list cannot be cyclic
class LL<T> ... {
ghost var Repr: set<object>
ghost predicate Invariant()
reads this, Repr
decreases Repr
{
&& this in Repr
&& (next != null ==>
&& next in Repr
&& next.Repr <= Repr
&& this !in next.Repr
&& next.Invariant())
}
}We strengthened the invariant
We need to review all the methods for which it is a postcondition
class LL<T> ... {
constructor OH(value: T)
ensures this.value == value
ensures this.next == null
ensures Invariant()
{
this.value := value;
next := null;
Repr := {this};
}
}This is a good strategy to develop verified data structures
Add methods one by one, strengthening invariant as you go, adapting existing code every time
class LL<T> ... {
method Cons(v: T) returns (l: LL<T>)
requires Invariant()
modifies Repr
ensures Invariant()
ensures l.Invariant()
{
l := new LL(v);
l.next := this;
l.Repr := Repr + {l};
}
}Now the invariant is strong enough for Length
In practice, there is a continuous co-design of invariant and code
class LL<T> ... {
function Length(): nat
requires Invariant()
reads Repr
decreases Repr
{
1 + if next == null then 0 else next.Length()
}
}Append is interesting because it involves two LLs
We need to require the LLs to be made of distinct objects
class LL<T> ... {
method Append(l: LL<T>)
requires next != null
requires Invariant()
requires l.Invariant()
modifies Repr
ensures Invariant()
}We do so with the frame rule
Here, Append requires some proof work
class LL<T> ... {
method Append(l: LL<T>)
requires next == null
requires Invariant()
requires Repr !! l.Repr
requires l.Invariant()
modifies Repr
ensures Invariant() // Fails
{
next := l;
Repr := Repr + l.Repr;
}
}forall c: LL :: c in old(Repr) ==> c !in l.Repr
The previous example is a common way to verify linked list
In Dafny, you can do much much better
Let's use dummy cells and a special root
class Cell<T> {
var next: Cell?<T>
var value: T
constructor(value: T)
ensures this.value == value
ensures this.next == null
{
this.value := value;
next := null;
}
}The LL will be defined as its root, as opposed to a cell
Here, Dafny shines: you can use any existing ghost data structure
Intuitively, we think of an LL as a sequence of cells
We can capture this directly in the representation!
Hence, we declare the representation to be a sequence
class LL<T> {
var length: nat
ghost var Repr: seq<Cell<T>>
var hd: Cell?<T>
}Again, we could grow the invariant
But with the additional structured dynamic frames, it is easier to capture our intuition
class LL<T> ... {
ghost predicate Invariant()
reads this, Repr
{
&& length == |Repr|
&& (length == 0 <==> hd == null)
&& (length > 0 ==> Repr[0] == hd)
&& (length > 0 ==> Repr[length-1].next == null)
&& (forall idx: nat :: idx < length - 1 ==>
Repr[idx].next != null
&& Repr[idx].next == Repr[idx+1]
)
}
}Nothing surprising, just need to initialize the dynamic frame
class LL<T> ... {
constructor()
ensures hd == null
ensures length == 0
ensures Invariant()
{
length := 0;
hd := null;
Repr := [];
}
} class LL<T> ... {
method Cons(v: T)
requires Invariant()
modifies this, Repr
ensures Invariant()
{
var o: Cell := new Cell(v);
o.next := hd;
hd := o;
Repr := [o] + Repr;
length := length + 1;
}
} class LL<T> ... {
method AppendNull(l: LL<T>)
requires length == 1
requires Invariant()
requires l.Invariant()
requires Repr[0] !in l.Repr
modifies this, Repr
ensures Invariant()
{
if l.length == 0 {
} else {
hd.next := l.hd;
Repr := Repr + l.Repr;
length := length + l.length;
}
}
}