Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:homework01 [2008/02/22 11:44] vkuncak |
sav08:homework01 [2009/03/11 17:22] vkuncak |
||
|---|---|---|---|
| Line 24: | Line 24: | ||
| } | } | ||
| </code> | </code> | ||
| - | You should be able to save this file as BinarySearchTree.scala, compile it with "scalac BinarySearchTree.scala", run it witn "scala BinarySearchTree", and obtain as a result "Inside". | + | You should be able to save this file as BinarySearchTree.scala, compile it with "scalac BinarySearchTree.scala", run it with "scala BinarySearchTree", and obtain as a result "Inside". |
| * for fun, test [[piVC tool]] and on BinarySearch.pi example (install piVC if needed) | * for fun, test [[piVC tool]] and on BinarySearch.pi example (install piVC if needed) | ||
| Line 30: | Line 30: | ||
| * you may also wish to check the tutorial and this [[http://afp.sourceforge.net/browser_info/current/HOL/BinarySearchTree/BinaryTree_TacticStyle.html|Binary Search Tree example]] | * you may also wish to check the tutorial and this [[http://afp.sourceforge.net/browser_info/current/HOL/BinarySearchTree/BinaryTree_TacticStyle.html|Binary Search Tree example]] | ||
| * for fun, Use formDecider.opt from [[:Jahob system]] to prove the same [[Proofs and Induction#Example|example from class]], as well as the examples in Exercises (install [[:Jahob system]] as well as provers CVC3 and E if needed) | * for fun, Use formDecider.opt from [[:Jahob system]] to prove the same [[Proofs and Induction#Example|example from class]], as well as the examples in Exercises (install [[:Jahob system]] as well as provers CVC3 and E if needed) | ||
| + | * if you log into your EPFL account, the Jahob verifier should be accessible by invoking: | ||
| + | <code> | ||
| + | ~kuncak/software/bin/verify --help | ||
| + | </code> | ||
| ===== Problem 1 ===== | ===== Problem 1 ===== | ||
| Line 90: | Line 94: | ||
| \lnot (p \land q) \leftrightarrow (\lnot p) \lor (\lnot q) \\ | \lnot (p \land q) \leftrightarrow (\lnot p) \lor (\lnot q) \\ | ||
| p \leftrightarrow \lnot (\lnot p) \\ | p \leftrightarrow \lnot (\lnot p) \\ | ||
| - | (p \rightarrow q) \leftrightarrow (p \lor (\lnot q)) \\ | + | (p \rightarrow q) \leftrightarrow ((\lnot p) \lor q) \\ |
| \lnot (p \lor q) \leftrightarrow (\lnot p) \land (\lnot q) | \lnot (p \lor q) \leftrightarrow (\lnot p) \land (\lnot q) | ||
| \end{array} | \end{array} | ||
| Line 99: | Line 103: | ||
| * generate a random assignment to propositional variables of the formula | * generate a random assignment to propositional variables of the formula | ||
| * compare the truth value of the original and of the transformed formula | * compare the truth value of the original and of the transformed formula | ||
| + | |||
| ===== Optional Problem 5 ===== | ===== Optional Problem 5 ===== | ||
| Line 104: | Line 109: | ||
| Consider [[:regular expression]]s with variables denoting subsets of $\Sigma^*$ where $\Sigma=\{0,1\}$. Define function $W$ that takes such a regular expression and replaces | Consider [[:regular expression]]s with variables denoting subsets of $\Sigma^*$ where $\Sigma=\{0,1\}$. Define function $W$ that takes such a regular expression and replaces | ||
| * each constant 0 with some relation $r_0$ and each constant 1 with some relation $r_1$ | * each constant 0 with some relation $r_0$ and each constant 1 with some relation $r_1$ | ||
| - | * for each variable $L$ denoting a subset of $\Sigma^*$, replaces all of its occurrences with some relation $r_L$ | + | * for each variable $L$ denoting a subset of $\Sigma^*$, replaces all of its occurrences with a relation variable $r_L$, denoting relations on $S$ |
| * replaces regular set union with relation union $\cup$ | * replaces regular set union with relation union $\cup$ | ||
| * replaces concatenation with relation composition $\circ$ | * replaces concatenation with relation composition $\circ$ | ||