LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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.