Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:homework07 [2008/04/10 16:33] vkuncak |
sav08:homework07 [2008/04/10 16:34] vkuncak |
||
|---|---|---|---|
| Line 15: | Line 15: | ||
| ===== Problem 2 ===== | ===== 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 features of the generated verifier. | + | 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. |
| Optional: insert checks that no result of arithmetic operation produces results whose absolute value is larger than 2^15-1. | Optional: insert checks that no result of arithmetic operation produces results whose absolute value is larger than 2^15-1. | ||