This is an old revision of the document!
Insertion into Doubly-Linked List
Doubly-linked list of size 3.
Code:
assume P; if (first == null) { first = n; n.next = null; n.prev = null; } else { n.next = first; first.prev = n; n.prev = null; first = n; } assert Q;
Where is \[\begin{array}{l}
n \neq null\ \land \\ next(n) = null \land prev(n)=null\ \land \\ prev(first) = null\ \land \ Q
\end{array} \] and where is \[\begin{array}{l}
\forall x.\forall y. prev(x)=y\ \ \rightarrow \\ \qquad (y \neq null \rightarrow next(y)=x)\ \land \\ \qquad (y = null \land x \neq null \rightarrow (\forall z. next(z) \neq x))
\end{array}\]
Corresponding Jahob file (call it dll-example.java).
We can check the add method by:
jahob.opt dll-example.java -method Simple.add -usedp cvcl
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:
- source code
- syntax tree
- jast: simplified statements (use option -jast to see it)
- ast: guarded commands with loops (use option -ast to see it)
- sast (use option -sast to see it):
- eliminating loops with loop invariants by translation to guarded commands (as in Backward VCG with Loops)
- incorporate preconditions and postconditions using assume and assert
- compute weakest precondition with respect to 'true' - this is verification condition (VC)
- simplify VC, split into multiple formulas, eliminate easily provable formulas
- use -v to view the remaining formulas
- use theorem provers to prove the resulting formulas
- some of the provers: cvcl (make symbolic link to cvc3), z3, SPASS, E, Vampire, BAPA, Isabelle (see also –help)
In general, system also deals with:
- specification variables (shorthands and ghost variables)
- loop invariant inference