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:31]
vkuncak created
+++ 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 ======
-<code java>
+Here is a [[simple linked list operation in Jahob]].
-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";
+What do verification conditions look like?
-     public vardefs "pointed == (% n. EX x. x ~= null & x..Node.next ~= n)";
-     invariant firstUnaliased: "first ~= null --> ~ pointed first";
+  tree [Node.next] --> F(Node.next)
-     invariant isTree: "tree [Node.next]";
-   */
-    public static void add(Node n)
+I will describe a decision procedure that can decide such formulas.
-    /*: 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>