Differences

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

--- sav08:homework07 [2008/04/10 16:34]
vkuncak
+++ sav08:homework07 [2008/04/11 09:58]
vkuncak
@@ Line 7: / Line 7: @@
 You may use current implementation homeworks as the starting point.
-A list of possible [[project suggestions]] will appear here soon, but you are free to choose your own.
+Here is a list of possible [[project suggestions]], but you are free to choose your own.
-Submit a project proposal of length 200-1000 words.  Summary project goal, why it is interesting, how you plan to solve it, and the difficulties you expect to encounter.
+Submit a project proposal of length 200-1000 words.  Summarize project goal, why it is interesting, how you plan to solve it, and the difficulties you expect to encounter.
-The proposal is not final, based on discussion with us you can reformulate the project.
+The proposal is not final--you can reformulate the project based on discussion with us.
 ===== Problem 2 =====
-Extend verification condition generator for integer programs from Problem 4 to handle procedures with supplied procedure specifications.  Connect the verification condition generator to a theorem prover using the SMT-LIB interface. You may use this code: {{sav08:decisionproc.scala.txt|DecisionProc.scala}}, generously provided from 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.  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.
+Extend verification condition generator for integer programs from [[Homework03]] to handle procedures with supplied procedure specifications as described in [[Lecture14]].
-Optional: insert checks that no result of arithmetic operation produces results whose absolute value is larger than 2^15-1.
+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 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, 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 number whose absolute value is larger than 2^15-1. Explore usability of the resulting system in practice.
 ===== Problem 3 =====