Differences

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

--- sav08:proving_correctness_of_some_small_examples [2008/02/17 17:20]
vkuncak created
+++ sav08:proving_correctness_of_some_small_examples [2010/02/23 12:31]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Proving Correctness of Some Small Examples ======
-{{sav08:integerdemo.java.txt|All Above Examples Working with Jahob}}
+In this demo we go through several examples and prove them correct using the [[:Jahob system]].
+==== A Recursive Function ====
+Consider the following recursive function:
+<code>
+private static int f(int x, int y)
+{
+  if (y == 0) {
+    return 0;
+  } else {
+    if (y % 2 == 0) {
+      int z = f(x, y / 2);
+      return (2 * z);
+    } else {
+      return (x + f(x, y - 1));
+    }
+  }
+}
+</code>
+  * What does 'f' compute?
+  * How can we prove it?
+  * [[Proof of first lecture01 example]]
+=== An Iterative Example ===
+<code>
+private static int fi(int x, int y)
+{
+  int r = 0;
+  int i = 0;
+  while
+    (i < y) {
+    i = i + 1;
+    r = r + x;
+  }
+  return r;
+}
+</code>
+  * How can we prove it?
+  * [[Notion of inductive loop invariant]]
+  * What is and is not inductive loop invariant in this example
+A verification condition formula for preserving an invariant:
+++++|
+\[
+    r = i * x \land i=i+1 \land r' = r + x \rightarrow r' = i' * x
+\]
+++++
+  * we will see methods to prove such invariants
+=== Transforming iterative version ===
+  * changing initial condition
+=== Summary of these Small Examples ===
+{{sav08:integerdemo.java.txt|Examples of Functions with Specifications}}
+=== Some other Examples done in Jahob ===
+  * http://javaverification.org/
+=== Another System ===
+  * [[http://research.microsoft.com/en-us/projects/vcc|VCC: A Verifier for Concurrent C]]