Differences

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

--- sav08:proving_correctness_of_some_small_examples [2008/02/17 18:37]
vkuncak
+++ sav08:proving_correctness_of_some_small_examples [2008/02/17 19:04]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Proving Correctness of Some Small Examples ======
-In this demo we go through several examples and prove them correct using Jahob.
+In this demo we go through several examples and prove them correct using the [[Jahob system]].
 ==== A Recursive Function ====
@@ Line 23: / Line 23: @@
 </code>
-{{sav08:integerdemo.java.txt|Examples of Functions with Specifications}}
+  * What does 'f' compute?
+  * How can we prove it?
+  * [[Proof of first lecture01 example]]
-For homework, you will have more such examples.
+=== 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
+=== Transforming iterative version ===
+=== Summary ===
+{{sav08:integerdemo.java.txt|Examples of Functions with Specifications}}
+For homework, you will have another such example.