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/07 14:42]
vkuncak
@@ Line 33: / Line 33: @@
 </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.
+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?
+  tree [Node.next] --> F(Node.next)
+I will describe a decision procedure that can decide such formulas.