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:18] vkuncak |
sav08:insertion_into_doubly-linked_list [2009/03/18 09:36] vkuncak |
||
---|---|---|---|
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 36: | Line 40: | ||
How can we build a verification conditions for such programs? | 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: | Illustration of phases in [[:Jahob system]] when loop invariants are specified: | ||
* 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: |