Lab for Automated Reasoning and Analysis 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?
 
introduction_to_using_msol_over_strings_to_verify_linked_lists.txt · Last modified: 2007/05/14 12:02 by vkuncak
 
© EPFL 2018 - Legal notice