Differences

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

--- sav07_homework_2 [2007/03/28 14:43]
vkuncak
+++ sav07_homework_2 [2007/03/30 13:56]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Homework 2 ======
@@ Line 22: / Line 24: @@
 For in depth understanding you can also read references in there, in particular the relevant Wilfrid Hodges model theory book sections.
+**Hint**: You should be able to reduce the problem to reasoning about conjunctions and generate a disjunction over total orders over terms of form v+c.  Alternatively, you may be able to use some ideas of [[http://citeseer.ist.psu.edu/71579.html|Fourier-Motzkin elimination]], but it is not necessary for this problem to have an efficient algorithm, only an algorithm that works in principle.
@@ Line 34: / Line 37: @@
       | havoc(v,...,v)
       | S ; S
-      | while (F) { S }
+      | while [inv F] (F) { S }
       | if (F) { S } else { S }
-  T ::= T+T | T-T | K*T | v
+  T ::= T+T | T-T | K*T | v | K
-  A ::= T=T | T < T
+  A ::= T=T | T < T | True | False
   F ::= A | (F&F) | (F|F) | ~F | ALL v.F | EX v.F
   K ::= 0 | 1 | 2 | ...
@@ Line 50: / Line 53: @@
 This notation corresponds to a fragment of the language of the [[wk>Isabelle theorem prover]], as well as the [[Jahob system]].
+The notation for while loop indicates that all loops have supplied loop invariants.
 You do not need to build a parser for programs and formulas for this exercise, but it may make the testing of your implementation easier.
-. Given a statement S, compute wp(S,true) and pretty print it as a string conforming to the above grammar.  Test your program on
+To make sure that you correctly avoid accidental variable capture, one of the many tests for your program should be the following 4 line sequence of commands:
+  x = 0;
+  y = x + 3;
+  havoc(x);
+  assert (y=3);
+. Given a statement S, compute wp(S,true) using the part 1, and pretty print it as a string conforming to the above grammar.  Test your program on
   * two input programs that generate valid formulas
   * two input programs that generate invalid formulas
 Try using the [[wk>Isabelle theorem prover]] or formDecider in the [[Jahob system]] to prove the validity of the printed formulas and describe your experience.