plt17:assignment_4

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

Both sides previous revision Previous revision Next revision | Previous revision | ||

plt17:assignment_4 [2017/11/02 12:04] hossein [Task 3] |
plt17:assignment_4 [2017/11/21 19:32] (current) hossein [Task 3] |
||
---|---|---|---|

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. | **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.1509638668.txt.gz ยท Last modified: 2017/11/02 12:04 by hossein