Differences

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

--- sav08:homework01 [2008/05/29 11:47]
barbara typo
+++ sav08:homework01 [2015/04/21 17:30]
@@ Line 1: / Line 1: @@
-====== Homework 01 ======
-===== Problem 0: Simple preparatory steps =====
-  * If you think you may attend the class, send emails to viktor.kuncak and ruzica.piskac saying that you plan to attend, so that we put you into system (e.g., wiki, grading).  If at any point you wish to be removed from our mailing list, we will of course do that promptly.
-  * Make sure you have access to a working [[http://www.scala-lang.org/|Scala language]] installation and learn how to use [[http://www.scala-lang.org/intro/caseclasses.html|Pattern Matching in Scala]].  Some very simple examples that use pattern matching is this binary search in Scala:
-<code>
-sealed abstract class BST {
-  def contains(key: Int): Boolean = (this : BST) match {
-    case Node(left: BST,value: Int, _) if key < value => left.contains(key)
-    case Node(_,value: Int, right: BST) if key > value => right.contains(key)
-    case Node(_,value: Int, _) if key == value => true
-    case e : Empty => false
-  }
-}
-case class Empty extends BST
-case class Node(val left: BST, val value: Int, val right: BST) extends BST
-object BinarySearchTree {
-  def main(args: Array[String]): Unit =
-    if (Node(Node(Empty(),3,Empty()),5,Empty()).contains(3)) println("Inside")
-    else println("Outside")
-}
-</code>
-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, use [[Isabelle theorem prover]] to prove the [[Proofs and Induction#Example|example from class]] (install Isabelle if needed)
-      * 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)
-  * if you log into your EPFL account, the Jahob verifier should be accessible by invoking:
-<code>
-~kuncak/software/bin/verify --help
-</code>
-===== Problem 1 =====
-Recall [[Proving Correctness of Some Small Examples]] from the class.  Consider the following annotated procedure that computes multiplication of arguments, but iterates backwards:
-<code>
-private static int fi3(int x, int y)
-/*: requires "x >= 0 & y >= 0"
-    ensures "result = x * y" */
-{
-  int r = 0;
-  int i = y;
-  while //: inv "..."
-     (i > 0) {
-    i = i - 1;
-    r = r + x;
-  }
-  return r;
-}
-</code>
-Write a loop invariant for this procedure that is sufficient to prove the postcondition //result = x * y//.  Prove that the invariant satisfies all three conditions in the [[Notion of Inductive Loop Invariant]].
-===== Problem 2 =====
-The following is a skeleton of an iterative version to the recursive procedure in [[Proving Correctness of Some Small Examples]].
-<code>
-private static int fip(int x, int y)
-/*: requires "x >= 0 & y >= 0"
-    ensures "result = x * y" */
-{
-  int y1 = y;
-  int a = x;
-  int r = 0;
-  while /*: inv "..." */
-     (y1 > 0) {
-    if (y1 % 2 != 0) {
-      r = ...
-      y1 = ...
-    }
-    y1 = ...
-    a = ...
-  }
-  return r;
-}
-</code>
-Complete the code with appropriate expressions, find the loop invariant, and prove that it satisfies all three conditions in the [[Notion of Inductive Loop Invariant]].
-===== Problem 3 =====
-Consider the definition of abstract syntax trees for [[Propositional Logic Informally|propositional formulas]] in [[http://scala-lang.org|Scala]], built from operators for negation, conjunction, disjunction, and implication.
-Write the evaluation function that takes a mapping from variable names to truth values and returns the truth value of the formula.
-You can find a skeleton that is a good starting point for this problem and the next one in file {{Propositional.scala.txt}} (remove the ".txt" file name suffix after saving the file).
-===== Problem 4 =====
-Negation-normal form of a propositional formula contains only conjunction, disjunction, and negation operators.  Such formula should not contain implication operator.  Moreover, negation only can only apply to variables and not to other formulas.  The following tautologies can be used to transform formula to negation normal form:
-\[\begin{array}{l}
-  \lnot (p \land q) \leftrightarrow (\lnot p) \lor (\lnot q) \\
-  p \leftrightarrow  \lnot (\lnot p) \\
-  (p \rightarrow q) \leftrightarrow ((\lnot p) \lor q) \\
-  \lnot (p \lor q) \leftrightarrow (\lnot p) \land (\lnot q)
-\end{array}
-\]
-Extend the solution for the previous problem with a function that takes formula syntax tree and transforms it into an equivalent formula in negation-normal form.  For example, the function should transform formula $\lnot (p \rightarrow \lnot q)$ into formula $p \land q$.
-Write also code that tests transformation to normal form by repeating several times the following steps:
-  * generate a random assignment to propositional variables of the formula
-  * compare the truth value of the original and of the transformed formula
-===== Optional Problem 5 =====
-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$
-  * for each variable $L$ denoting a subset of $\Sigma^*$, replaces all of its occurrences with some relation $r_L$
-  * replaces regular set union with relation union $\cup$
-  * replaces concatenation with relation composition $\circ$
-  * replaces language iteration star with transitive closure $*$
-For example
-\[
-   W({(p+qp)*}\, p) = (r_p \cup (r_q \circ r_p))^* \circ r_p
-\]
-Is it the case that that if an equality $r_1 = r_2$ holds for all values of variables representing subsets of $\Sigma^*$, then $W(r_1) = W(r_2)$ holds for all values of relation variables?  If so, prove it.  If not, give a counterexample.