Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
verifying_data_structures_using_jahob [2007/06/15 14:54] kremena.diatchka |
verifying_data_structures_using_jahob [2007/06/21 11:53] kremena.diatchka |
||
|---|---|---|---|
| Line 9: | Line 9: | ||
| * Linked list with header node | * Linked list with header node | ||
| * Queue (partial specification) | * Queue (partial specification) | ||
| - | * Cyclic list (almost?) | + | * Cyclic list (probable bug with verification of initial state) |
| ==== In progress ==== | ==== In progress ==== | ||
| * Leaf-linked tree | * Leaf-linked tree | ||
| - | * Checking why cyclic list doesn't verify in initial state | + | |
| + | Implementation done, some class invariants written. TO DO: focus on expanding specifications: procedure contracts and loop invariants. | ||
| + | |||
| + | * Doubly-linked cyclic list | ||
| + | |||
| + | Init() and add() methods verify, problem with loop invariant for member method. | ||