This is an old revision of the document!
Verifying data structures using Jahob
by Feride Cetin and Kremena Diatchka
Our goal is to verify the implementations in Java of simple data structures using Jahob.
Verified
- Linked list with header node
- Queue (partial specification)
- Cyclic list (probable bug with verification of initial state)
In progress
- Leaf-linked tree
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.