Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision Next revision Both sides next revision | ||
|
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/07 14:42] 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 a method and its annotation in the Jahob verification system. | ||
| <code java> | <code java> | ||
| Line 30: | Line 32: | ||
| } | } | ||
| </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 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. | ||