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 Scala language installation and learn how to use Pattern Matching in Scala. Some very simple examples that use pattern matching is this binary search in Scala:

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")
}

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 example from class (install Isabelle if needed)
- you may also wish to check the tutorial and this Binary Search Tree example
for fun, Use formDecider.opt from Jahob system to prove the same 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:

~kuncak/software/bin/verify --help

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:

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;
}

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.

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;
}

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 formulas in 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{equation*}\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} \end{equation*}$

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 expressions 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 a relation variable $r_L$ , denoting relations on $S$
replaces regular set union with relation union $\cup$
replaces concatenation with relation composition $\circ$
replaces language iteration star with transitive closure $*$

For example

$\begin{equation*} W({(p+qp)*}\, p) = (r_p \cup (r_q \circ r_p))^* \circ r_p \end{equation*}$

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.