LARA

This is an old revision of the document!


Introduction to using MSOL over strings to verify linked data structures

The following is an example of a method and its annotation in the Jahob verification system.

class Node {
    public /*: claimedby List */ Node next;
}
class List
{
   private static Node first;  
   /*:
     public static specvar content :: objset;
     vardefs "content == {x. x ~= null & (first,x) : {(v,w). v..Node.next=w}^*}";
 
     public static specvar pointed :: "obj => bool";
     public vardefs "pointed == (% n. EX x. x ~= null & x..Node.next = n)";
 
     invariant firstUnaliased: "first ~= null --> ~ pointed first";
     invariant isTree: "tree [Node.next]";
   */
 
    public static void add(Node n)
    /*: requires "n ~: content & n ~= null & n..Node.next = null & ~ pointed n"
        modifies content, pointed
        ensures "comment ''post'' (content = old content Un {n})"
    */
    {
	n.next = first;
	first = n;
    }
}

It is an ordinary Java code with some annotations written in comments. The code manipulates a singly linked list of 'Node' elements. The specification variable 'content' stores all non-null objects reachable from the static variable 'first'. The definition of 'content' uses set comprehension notation '{(v,w). …}' and transitive closure notation 'r^*' to define the set of non-null nodes reachable from the first element.

The 'pointed' shorthand is a predicate that is true for a node 'n' if another node 'x' points to it. The 'pointed' predicate is defined using lambda expression for defining functions.

Automated verification of properties that involve reachability is a very difficult problem in general. The reason why it is possible in our case is that we are requiring the invariant 'tree [Node.next]' whose meaning is:

  • there are never two objects that point to the same object along Node.next field
  • there are no cycles of 'Node.next' fields

Such invariants can be generalized to trees, but we first examine the case of lists.

What do verification conditions look like?

tree [Node.next] --> F(Node.next)

I will describe a decision procedure that can decide such formulas.