Differences
This shows you the differences between two versions of the page.
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 13:36] 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 '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. | ||