LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:homework07 [2008/04/10 19:28]
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.
  
-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 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.  ​ 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 ​integerssatisfies 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 =====