Differences

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

--- sav08:homework07 [2008/04/10 19:28]
vkuncak
+++ sav08:homework07 [2008/04/10 19:29]
vkuncak
@@ Line 19: / Line 19: @@
 Connect the verification condition generator to a theorem prover using the SMT-LIB interface. In your solution you may use this code {{sav08:decisionproc.scala.txt|DecisionProc.scala}}, generously provided by Damien from his previous homework.
-Your resulting program should be able to check whether program, defined as a collection of procedures manipulating integers, satisfies given preconditions and postconditions.
+Your resulting program should be able to check whether a given collection of recursive procedures that manipulate integers satisfies given preconditions and postconditions.  Provide at least 3 test cases that illustrate the capabilities of the system.
-For simplicity, you may assume that procedures do not return results and procedure calls are statements, not parts of expressions.  There is no need to write a parser, use syntax trees, but do provide at least 3 test cases that illustrate the capabilities of the system.
+For simplicity, you may assume that procedures do not return results, only accept parameters and change global state.  There is no need to write a parser, use syntax trees.
-**Optional:** insert assertions that check that no result of arithmetic operation produces results whose absolute value is larger than 2^15-1 and explore usability of the resulting system in practice.
+**Optional:** insert assertions that check that no result of arithmetic operation produces number whose absolute value is larger than 2^15-1. Explore usability of the resulting system in practice.
 ===== Problem 3 =====