User Tools

Site Tools


plt17:assignment_4

Differences

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

Link to this comparison view

Next revision
Previous revision
plt17:assignment_4 [2017/10/31 20:54]
hossein created
plt17:assignment_4 [2017/11/21 19:32] (current)
hossein [Task 3]
Line 17: Line 17:
 |      |   ​|//​Id//​ := //IExp// | |      |   ​|//​Id//​ := //IExp// |
 |      |   ​|//​Stmt//​ **;** //Stmt// | |      |   ​|//​Stmt//​ **;** //Stmt// |
-|      |   |**if (** //BExp// **)** //Stmt// **else** //​Stmt// ​ +|      |   |**if (** //BExp// **)** //Stmt// **else** //​Stmt// ​**endif** ​
-|      |   ​|**while (** //BExp// **)** //​Stmt// ​ |+|      |   ​|**while (** //BExp// **)** //​Stmt// ​**endwhile** ​|
 |      |   ​|**assert (** //BExp// **)** | |      |   ​|**assert (** //BExp// **)** |
 |  //​BExp//​|::​=| //IExp// **<=** //IExp// | |  //​BExp//​|::​=| //IExp// **<=** //IExp// |
Line 58: Line 58:
 ===== Task 3 ===== ===== Task 3 =====
  
-Verify ​the input program by checking the satisfiability of the generated Horn solvers by consulting ​an off-the-shelf Horn solver (e.g. [[https://​github.com/​Z3Prover/​z3|Z3]],​ [[https://​github.com/​uuverifiers/​eldarica|Eldarica]] ​ or [[https://​bitbucket.org/​spacer/​|Spacer]]). ​+When the user calls your program ​with the -v argument, it will verify the input file by checking the satisfiability of the generated Horn clauses. For satisfiability you can consult ​an off-the-shelf Horn solver (e.g. [[https://​github.com/​Z3Prover/​z3|Z3]],​ [[https://​github.com/​uuverifiers/​eldarica|Eldarica]] ​ or [[https://​bitbucket.org/​spacer/​|Spacer]]). ​
 Your program will either print ''​correct''​ for a program with no bug.  Your program will either print ''​correct''​ for a program with no bug. 
 Or, it will write ''​incorrect''​ for a program that has bug. Or, it will write ''​incorrect''​ for a program that has bug.
Line 64: Line 64:
  
 **Bonus** Print out the values under which the program will hit the error. **Bonus** Print out the values under which the program will hit the error.
 +
 +**Note** You can either install the theorem prover on your machine and your code executes the theorem prover ​ as an external application (i.e. z3 can be called from the command line), or you can add the required libraries to call the theorem prover from its libraries.
 ===== Task 4 (Bonus) ===== ===== Task 4 (Bonus) =====
  
plt17/assignment_4.1509497661.txt.gz · Last modified: 2017/10/31 20:54 by hossein