Differences

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

--- introduction_to_using_msol_over_strings_to_verify_linked_lists [2007/05/07 13:36]
vkuncak
+++ introduction_to_using_msol_over_strings_to_verify_linked_lists [2007/05/14 12:02]
vkuncak
@@ Line 1: / Line 1: @@
 ====== 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.
+Here is a [[simple linked list operation in Jahob]].
-<code java>
+What do verification conditions look like?
-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";
+  tree [Node.next] --> F(Node.next)
-     public vardefs "pointed == (% n. EX x. x ~= null & x..Node.next ~= n)";
-     invariant firstUnaliased: "first ~= null --> ~ pointed first";
+I will describe a decision procedure that can decide such formulas.
-     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;
-    }
-}
-</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 '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.