Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:insertion_into_doubly-linked_list [2009/03/18 09:18] vkuncak |
sav08:insertion_into_doubly-linked_list [2009/03/18 09:21] vkuncak |
||
|---|---|---|---|
| Line 36: | Line 36: | ||
| How can we build a verification conditions for such programs? | How can we build a verification conditions for such programs? | ||
| + | * we need to be able to reason about **data structures** (objects, references, arrays) | ||
| Illustration of phases in [[:Jahob system]] when loop invariants are specified: | Illustration of phases in [[:Jahob system]] when loop invariants are specified: | ||