Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
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/09 22:45] vkuncak |
||
---|---|---|---|
Line 12: | Line 12: | ||
/*: | /*: | ||
public static specvar content :: objset; | public static specvar content :: objset; | ||
- | private vardefs "content == {x. (first,x) : {(v,w). first ~= null & v..Node.next=w}^*}"; | + | vardefs "content == {x. x ~= null & (first,x) : {(v,w). v..Node.next=w}^*}"; |
public static specvar pointed :: "obj => bool"; | public static specvar pointed :: "obj => bool"; | ||
- | public vardefs "pointed == (% n. EX x. x ~= null & x..Node.next ~= n)"; | + | public vardefs "pointed == (% n. EX x. x ~= null & x..Node.next = n)"; |
invariant firstUnaliased: "first ~= null --> ~ pointed first"; | invariant firstUnaliased: "first ~= null --> ~ pointed first"; | ||
Line 23: | Line 23: | ||
public static void add(Node n) | public static void add(Node n) | ||
/*: requires "n ~: content & n ~= null & n..Node.next = null & ~ pointed n" | /*: requires "n ~: content & n ~= null & n..Node.next = null & ~ pointed n" | ||
- | modifies content | + | modifies content, pointed |
- | ensures "content = old content Un {n}" | + | ensures "comment ''post'' (content = old content Un {n})" |
*/ | */ | ||
{ | { | ||
Line 33: | Line 33: | ||
</code> | </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. | ||