Differences

This shows you the differences between two versions of the page.

--- sav08:insertion_into_doubly-linked_list [2009/03/17 23:15]
vkuncak
+++ sav08:insertion_into_doubly-linked_list [2009/03/18 09:36]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Insertion into Doubly-Linked List ======
+(Figure of doubly-linked list of size 3.)
+Code:
 <code>
@@ Line 30: / Line 34: @@
 \end{array}\]
-Corresponding {{sav08:simpledll.java.txt|Jahob file}} which verifies quickly using e.g.
+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