LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
introduction_to_using_msol_over_strings_to_verify_linked_lists [2007/05/09 22:45]
vkuncak
introduction_to_using_msol_over_strings_to_verify_linked_lists [2007/05/14 12:02] (current)
vkuncak
Line 1: Line 1:
 ====== Introduction to using MSOL over strings to verify linked data structures ====== ====== Introduction to using MSOL over strings to verify linked data structures ======
  
-The following ​is an example of method and its annotation in the Jahob verification system. +Here is a [[simple ​linked list operation in Jahob]].
- +
-<code java> +
-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; +
-    } +
-+
-</​code>​ +
- +
-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 calculus|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? What do verification conditions look like?