Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:homework07 [2008/04/10 19:21] vkuncak |
sav08:homework07 [2008/04/11 09:58] vkuncak |
||
---|---|---|---|
Line 7: | Line 7: | ||
You may use current implementation homeworks as the starting point. | 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. Summarize 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. | ||
Line 15: | Line 15: | ||
===== Problem 2 ===== | ===== Problem 2 ===== | ||
- | Extend verification condition generator for integer programs from [[Homework03]] to handle procedures with supplied procedure specifications as described in [[Lecture04]]. | + | Extend verification condition generator for integer programs from [[Homework03]] to handle procedures with supplied procedure specifications as described in [[Lecture14]]. |
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. | 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 ===== | ===== Problem 3 ===== |