Differences
This shows you the differences between two versions of the page.
sav08:insertion_into_doubly-linked_list [2009/03/18 09:35] vkuncak |
sav08:insertion_into_doubly-linked_list [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Insertion into Doubly-Linked List ====== | ||
- | |||
- | Doubly-linked list of size 3. | ||
- | |||
- | Code: | ||
- | |||
- | <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; | ||
- | </code> | ||
- | |||
- | Where $P$ 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 $Q$ 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 {{sav08:simpledll.java.txt|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 | ||