Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
introduction_to_using_msol_over_strings_to_verify_linked_lists [2007/05/07 14:42] 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})" |
| */ | */ | ||
| { | { | ||