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; private vardefs "content == {x. (first,x) : {(v,w). first ~= null & 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 ensures "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 '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.