Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:insertion_into_doubly-linked_list [2009/03/18 09:21] vkuncak |
sav08:insertion_into_doubly-linked_list [2015/04/21 17:30] (current) |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Insertion into Doubly-Linked List ====== | ====== Insertion into Doubly-Linked List ====== | ||
| + | |||
| + | (Figure of doubly-linked list of size 3.) | ||
| + | |||
| + | Code: | ||
| <code> | <code> | ||
| Line 17: | Line 21: | ||
| Where $P$ is | Where $P$ is | ||
| - | \[\begin{array}{l} | + | \begin{equation*}\begin{array}{l} |
| n \neq null\ \land \\ | n \neq null\ \land \\ | ||
| next(n) = null \land prev(n)=null\ \land \\ | next(n) = null \land prev(n)=null\ \land \\ | ||
| prev(first) = null\ \land \ Q | prev(first) = null\ \land \ Q | ||
| \end{array} | \end{array} | ||
| - | \] | + | \end{equation*} |
| and where $Q$ is | and where $Q$ is | ||
| - | \[\begin{array}{l} | + | \begin{equation*}\begin{array}{l} |
| \forall x.\forall y. prev(x)=y\ \ \rightarrow \\ | \forall x.\forall y. prev(x)=y\ \ \rightarrow \\ | ||
| \qquad (y \neq null \rightarrow next(y)=x)\ \land \\ | \qquad (y \neq null \rightarrow next(y)=x)\ \land \\ | ||
| \qquad (y = null \land x \neq null \rightarrow (\forall z. next(z) \neq x)) | \qquad (y = null \land x \neq null \rightarrow (\forall z. next(z) \neq x)) | ||
| - | \end{array}\] | + | \end{array}\end{equation*} |
| Corresponding {{sav08:simpledll.java.txt|Jahob file}} (call it dll-example.java). | Corresponding {{sav08:simpledll.java.txt|Jahob file}} (call it dll-example.java). | ||
| Line 41: | Line 45: | ||
| * source code | * source code | ||
| * syntax tree | * syntax tree | ||
| - | * jast: simplified statements | + | * jast: simplified statements (use option -jast to see it) |
| - | * ast: guarded commands with loops | + | * ast: guarded commands with loops (use option -ast to see it) |
| - | * sast: | + | * sast (use option -sast to see it): |
| * eliminating loops with loop invariants by translation to guarded commands (as in [[Backward VCG with Loops]]) | * eliminating loops with loop invariants by translation to guarded commands (as in [[Backward VCG with Loops]]) | ||
| * incorporate preconditions and postconditions using assume and assert | * incorporate preconditions and postconditions using assume and assert | ||
| * compute weakest precondition with respect to 'true' - this is verification condition (VC) | * compute weakest precondition with respect to 'true' - this is verification condition (VC) | ||
| * simplify VC, split into multiple formulas, eliminate easily provable formulas | * 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 | * 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: | In general, system also deals with: | ||