\documentclass{article}

\title{COMP2111 Assignment 2 \\ Solutions}
\date{1-5-2016}
\author{Mazen Kourouche (z5059155), Anna Azzam (z3470058)}
\usepackage{amsmath}
\usepackage{units}
\usepackage{amssymb}
\usepackage{mathtools}
\usepackage{enumerate}
\usepackage{xcolor}

\begin{document}
\pagenumbering{gobble}
\maketitle
\newpage
\pagenumbering{arabic}



\section{Specification Statement}
The function is specified by:
\begin{equation*}
    proc \enspace  Em \enspace (value \enspace n,  result \enspace  E)
\end{equation*}
Specification statement is:
\begin{equation*}
    i : [n \in \mathbb{N} \enspace , \enspace E = Emirp(n)]
\end{equation*}
Where:
\begin{equation*}
    Emirp(N) = \forall i \in [2, N] \enspace \cdot \enspace (isPrime(i) \enspace \land \enspace isPrime(reverse(i)) \enspace \land \enspace (i \neq reverse(i))
\end{equation*}
\begin{equation*}
    isPrime(X) = \forall i \in [2, X) \cdot ((x \enspace mod \enspace i) \neq 0)
\end{equation*}
And assuming reverse(I) is a method provided which reverses a number I





   \section{Refinement}
   We started off with our specification statement and used refinement laws to derive our C function emirp. Any implications required during the refinement are proved below. \newline \newline

   \subsection{Proof for main refinement}

   Let \textbf{P} be equivalent to $ (nEmirps \leq n) \land (i \geq 2) $ \textbf{(Loop invariant)}. \newline

   $i : [n \in \mathbb{N} , \enspace Emirp(n)]$ \newline\\
   $\sqsubseteq \enspace var\enspace nEmirps : \mathbb{N} \enspace \cdot \enspace \textcolor{red}{\llcorner} i, nEmirps : [n \in \mathbb{N},  \enspace Emirp(n)]  \textcolor{red}{\lrcorner} $ \textbf{(i-loc rule)} \newline
   $\textcolor{red}{\sqsubseteq} \enspace \textcolor{blue}{\llcorner} i, nEmirps : [n \in \mathbb{N}, \enspace P] \textcolor{blue}{\lrcorner}
   \enspace \textbf{;} \enspace \textcolor{green}{\llcorner}  i, nEmirps :[P, \enspace Emirp(n)] \textcolor{green}{\lrcorner}$ \textbf{(seq)} \newline
   $ \textcolor{blue}{\sqsubseteq} \enspace  i, nEmirps : [n \in \mathbb{N}, \enspace P[\nicefrac{0}{nEmirps}]] \enspace \textbf{;} \enspace
    i, nEmirps [P[\nicefrac{0}{nEmirps}], \enspace P] $ \textbf{(seq)} \newline
   $\sqsubseteq \enspace nEmirps := 0\enspace  ; \enspace i, nEmirps : [P[\nicefrac{0}{nEmirps}], \enspace P] $ \textbf{(ass, see impl. 1)} \newline
   $\sqsubseteq \enspace nEmirps := 0 \enspace \textbf{;} \enspace i := 2 $ \textbf{(ass, see impl. 2)} \newline\\
   $\textcolor{green}{\sqsubseteq} \enspace while \enspace (nEmirps < n) \enspace do \newline
   \indent \textcolor{green}{\llcorner}  i, nEmirps : [(nEmirps < n ) \land P, \enspace P] \textcolor{green}{\lrcorner} \newline
   done $ \textbf{(while rule, see impl. 3)} \newline\\
   $\textcolor{green}{\sqsubseteq} \enspace var \enspace j : \mathbb{N} \enspace \cdot \enspace \textcolor{green}{\llcorner} i, j, nEmirps:[(nEmirps < n) \land P, \enspace P] \textcolor{green}{\lrcorner} $ \textbf{(i-loc)} \newline
   $\textcolor{green}{\sqsubseteq} \enspace i, j, nEmirps : [(nEmirps < n) \land P, \enspace P \land ((i != j) \vee (i = j))] \enspace \textbf{;} \newline
   \indent \indent \indent i, j, nEmirps : [P \land (i = j \vee i != j), \enspace P] $ \textbf{(seq)} \newline
   $\sqsubseteq \enspace j := reverse(i) \enspace \textbf{;} \newline
   \indent \indent \indent \textcolor{green}{\llcorner}  i, j, nEmirps : [P \land (i = j \vee i != j), \enspace P] \textcolor{green}{\lrcorner} $ \textbf{(ass, see impl. 4)} \newline
   $\textcolor{green}{\sqsubseteq} \enspace i, j, nEmirps : [P \land (i = j \vee i != j), \enspace P[\nicefrac{i+1}{i}]] \enspace \textbf{;} \newline
   \indent \indent \indent  i, j, nEmirps : [P[\nicefrac{i+1}{i}], \enspace P] $ \textbf{(seq)} \newline
   $\sqsubseteq  \textcolor{green}{\llcorner} i, j, nEmirps : [P \land (i = j \vee i != j), \enspace P[\nicefrac{i+1}{i}]] \textcolor{green}{\lrcorner} \enspace \textbf{;} \newline
   \indent \indent \indent  i := i + 1  $ \textbf{(ass, see impl. 5)} \newline\\
   $\textcolor{green}{\sqsubseteq} \enspace if \enspace (i != j) \enspace then \newline
   \indent \textcolor{green}{\llcorner}  i, j, nEmirps :[P \land (i != j), \enspace P[\nicefrac{i+1}{i}]]   \textcolor{green}{\lrcorner} \newline
   fi $ \textbf{(if1, see impl. 6)} \newline\\
   $\textcolor{green}{\sqsubseteq} \enspace i, j, nEmirps : [P \land (i != j) \enspace \land \enspace ((isPrime(i) \land isPrime(j)) \newline \indent \indent \indent \vee (\neg isPrime(i) \vee \neg isPrime(j))), \enspace P[\nicefrac{i+1}{i}]] $ \textbf{(w-pre, see impl. 7)} \newline\\
   $\sqsubseteq \enspace if \enspace (isPrime(i) \land isPrime(j)) \enspace then \newline
   \indent \textcolor{green}{\llcorner} i, j, nEmirps : [P \land (i!= j) \land (isPrime(i) \land isPrime(j)), \enspace P[\nicefrac{i+1}{i}]] \textcolor{green}{\lrcorner} \newline
   fi $ \textbf{(if 1, see impl. 8)} \newline\\
   $\textcolor{green}{\sqsubseteq} \enspace nEmirps := nEmirps + 1 $ \textbf{(ass, see impl. 9)} \newline\\

   \noindent \textbf{Therefore the final code is:} \newline
   $var \enspace nEmirps \newline
   var\enspace  i \newline
   nEmirps := 0 \newline
   i := 2 \newline
   while \enspace (nEmirps < n) \enspace do \newline
   \indent var j \newline
   \indent j := reverse (i) \newline
   \indent if \enspace (i != j) \enspace then \newline
   \indent \indent if \enspace (isPrime(i) \land isPrime(j)) \enspace then \newline
   \indent \indent \indent nEmirps := nEmirps + 1 \newline
   \indent \indent fi \newline
   \indent fi \newline
   \indent i := i + 1 \newline
   od
   $


   \subsection{Proof for isPrime}

    $\gamma:[n \in \mathbb{N},  \enspace \gamma = isPrime(n)]$\\\\
    $\sqsubseteq \enspace var  \enspace i: \mathbb{N}  \enspace \cdot  \enspace \textcolor{green}{\llcorner}\gamma, i:[n \in \mathbb{N}, \gamma = isPrime(n)] \textcolor{green}{\lrcorner}$ \textbf{(i-loc rule)} \\
    $\textcolor{green}{\sqsubseteq} \enspace \gamma, i:[n \in \mathbb{N}, \gamma = isPrime(i) \wedge i < n];$\\
    $ \indent\gamma, i:[\gamma = isPrime(i) \wedge i<n, \gamma = isPrime(n)]$\\
    $\indent \gamma:[n \in \mathbb{N},  \enspace \gamma = isPrime(n)]$\\\\
    $\enspace\sqsubseteq \enspace var \enspace i, iP: \mathbb{N} \cdot \textcolor{blue}{\llcorner}\gamma, \, iP: [n \in \mathbb{N}, \gamma = isPrime(n, i, iP)]\textcolor{green}{\lrcorner}$ \textbf{(i-loc rule)} \\
    $\textcolor{blue}{\sqsubseteq} \enspace \gamma, i, iP: \textcolor{red}{\llcorner}[n \in \mathbb{N}, \gamma = isPrime(n, i, iP) \enspace \wedge \enspace iP \in [0,1] \wedge i \leqslant n]\textcolor{red}{\lrcorner}$ \textbf{(s-post)}\\
    $\textcolor{red}{\sqsubseteq} \enspace \gamma, i, iP: [n \in \mathbb{N},  iP \in [0,1] \wedge i \leqslant n];$\\
    $\indent \enspace \textcolor{purple}{\llcorner}\gamma, i, iP: [\enspace iP \in [0,1] \wedge i \leqslant n \enspace \wedge \enspace \gamma = isPrime(n, i, iP)]\textcolor{purple}{\lrcorner}$ \textbf{(seq)}\\
    $\textcolor{purple}{\sqsubseteq} \enspace i:=0$ \textbf{(ass)} \\
    $\indent iP:=1$ \textbf{(ass)} \\
    $\indent \gamma, i, iP:[n \in \mathbb{N}, iP \in [0,1] \wedge i \leqslant n]$\\\\
    $\sqsubseteq \enspace while \enspace(i < n) \enspace do \enspace P \enspace od$
    $P:[i<n \wedge i \in \mathbb{N}, iP \in [0,1]]$ \textbf{(while rule)}\\\\
    $\noindent \sqsubseteq \enspace if ((Mod(n, i) = 0) \enspace then \enspace \textcolor{green}{\llcorner}w:[(Mod(n,i) = 0 \enspace \wedge \enspace (i<n \enspace \wedge \enspace i \in \mathbb{N}), \enspace iP = 0]\textcolor{green}{\lrcorner} \enspace else \enspace \textcolor{blue}{\llcorner}w:[(Mod(n,i)!=0) \enspace \wedge \enspace i < N \enspace \wedge i \in \mathbb{N} \enspace \wedge \enspace iP \in [0,1] \enspace \wedge \enspace i \leqslant n]\textcolor{blue}{\lrcorner} \enspace fi$ \textbf{(if)}\\\\
    $\sqsubseteq \enspace iP:=1$ \textbf{(ass)} \\
    $w:[(Mod(n,i) = 0 \enspace \wedge (i < n \wedge i \in \mathbb{N}), iP = 0]$\\\\
    $\sqsubseteq \enspace i:=i+1$ \textbf{(ass)} \\
    $w:[(Mod(n,i) != 0 \enspace \wedge i < n \wedge i \in \mathbb{N} \enspace \wedge iP \in [0,1], i \leqslant n]$\\\\
    \textbf{Therefore the final code is:}\\
    $var \enspace i$\\
   $ var \enspace iP$\\
    $i:=0$\\
    $iP:=1$\\
    $while (i<n) do$\\
    \indent $if (Mod(n,i) == 0) \enspace then$\\
        \indent\indent$iP:=0$ \enspace $else $\\
    \indent \indent $ i:=i+1$\\
        \indent$fi$\\
    $od$




\subsection{Implications}
\subsubsection{Implication 1}
To use the \textbf{assignment rule}, we need to prove that $w = w_0$ which is true since E does not change, and \newline
$pre \Rightarrow post[\nicefrac{e}{w}]$, \newline
i.e. $n \in \mathbb{N} \enspace \Rightarrow \enspace P[\nicefrac{0}{nEmirps}][\nicefrac{0}{nEmirps}]$ \newline\\
Assuming LHS true, RHS $\Leftrightarrow (0 \leq n \land i \geq 2)$ \newline
$\Leftrightarrow True \land True$ since
\begin{itemize}
    \item Pre-condition states $n \in \mathbb{N} $ therefore $n \geq 0$
    \item i is initialised to be 2 and is never decremented, therefore $i \geq 2$
\end{itemize}
$\therefore pre \Rightarrow post[\nicefrac{e}{w}]$ is true,  justifying the use of the assignment rule.


\subsubsection{Implication 2}
To use the \textbf{assignment rule}, we need to prove that $w = w_0$ which is true, and
$pre \Rightarrow post[\nicefrac{e}{w}]$, \newline
i.e. $P[\nicefrac{0}{nEmirps}] \Rightarrow P[\nicefrac{2}{i}]$ \newline\\
LHS $\Rightarrow n \geq 0 \land i \geq 2$ \newline
$\therefore$ Assuming LHS true, RHS $\Leftrightarrow$ \newline
$ (nEmirps \leq n) \land (2 \geq 2)$ \newline
$\Leftrightarrow True \land True$ since
\begin{itemize}
    \item Loop guard ensures nEmirps $<$ n \newline
    $\therefore$ nEmirps $\leq$ n is always true
    \item $2 \geq 2$  is obviously true
\end{itemize}
$\therefore pre \Rightarrow post[\nicefrac{e}{w}]$ is true, justifying the use of the assignment rule.


\subsubsection{Implication 3}
To use the \textbf{while rule}, we need to prove that $[P, Emirp(n)]$ is equivalent to $[inv, inv \land \neg g]$ where \newline
\begin{itemize}
    \item $ g = (nEmirps < n)$, and
    \item inv = P
\end{itemize}
PRE-CONDITIONS: $P \Leftrightarrow inv$ is obviously true. \newline\\
POST-CONDITIONS: Show that \newline
$Emirp(n) \Rightarrow P \land \neg(nEmpirps < n)$ \newline
$RHS \Leftrightarrow (nEmirps \leq n) \land (i \geq 2) \land (nEmirps \geq n)$ \newline
$\Leftrightarrow (nEmirps = n) \land (i \geq 2)$ \newline
$\Leftrightarrow True \land True \Leftrightarrow True$, since
\begin{itemize}
    \item Loop only exits once $nEmirps = n$, \newline
    $\therefore nEmirps = n$ is true.
    \item  i is initialised to be 2 and is never decremented, therefore $i \geq 2$
\end{itemize}
$\therefore LHS \Rightarrow RHS$, justifying the use of the while rule.


\subsubsection{Implication 4}
To use the \textbf{assignment rule}, we need to prove that $w = w_0$ which is true, and
$pre \Rightarrow post[\nicefrac{e}{w}]$, \newline
i.e. $P \land (i = j \vee i != j) \Rightarrow P[\nicefrac{reverse(i)}{j}]$ \newline\\
$LHS \Rightarrow (P \land True)$, since $(i = j \vee i != j)$ is always true by \textbf{and with complement}. \newline
$\Rightarrow True$ \newline\\
$RHS \Rightarrow (nEmirps \leq n) \land (i \geq 2)$ \newline
$\Leftrightarrow P$ \newline
$\therefore LHS \Rightarrow RHS$ is true.


\subsubsection{Implication 5}
We need to show that $pre \Rightarrow post[\nicefrac{i+1}{i}]$ \newline
i.e.$ P[\nicefrac{i+1}{i}] /Rightarrow P[\nicefrac{i+1}{i}]$ \newline
which is obviously true.


\subsubsection{Implication 6}
To use the \textbf{if1 rule}, we need to prove that \newline
$[P \land (i = j \vee i != j), \enspace P[\nicefrac{i+1}{i}]]$ implies \newline
$[(g \land \phi) \vee (\neg g \land \psi[\nicefrac{w}{w_0}], \enspace \psi]$, where
\begin{itemize}
    \item $\psi \enspace is \enspace P[\nicefrac{i+1}{i}]$, and
    \item $g \enspace is \enspace (i != j)$
\end{itemize}
POST-CONDITIONS: $P[\nicefrac{i+1}{i}] \Rightarrow \psi$ is obviously true. \newline\\
PRE-CONDITIONS: Let $\psi \Leftrightarrow True$. \newline
$RHS \Rightarrow (i != j \land True) \vee (i = j \land P[\nicefrac{i+1}{i}]$ \newline
$\Rightarrow (i != j) \vee ((i = j) \land P[\nicefrac{i+1}{i}])$ \newline
$\therefore LHS \Rightarrow RHS$ since \newline
$i \geq 2 \Rightarrow i \geq 1 \newline \therefore P \Rightarrow P[\nicefrac{i+1}{i}]$ is True.
Thus justifying the use of the if1 rule.


\subsubsection{Implication 7}
To prove the use of the \textbf{w-pre rule} we need to show that \newline
$P \land (i != j) \Rightarrow \newline
\indent P \land (i != j) \land ((isPrime(i) \land isPrime(j)) \vee (\neg isPrime(i) \vee \neg isPrime(j)))$ \newline\\
Assuming LHS is true, \newline
$RHS \Leftrightarrow True \land ((isPrime(i) \land isPrime(j)) \vee (\neg isPrime(i) \vee \neg isPrime(j)))$ \textbf{(by subbing in LHS)} \newline
$\Leftrightarrow True \land True$ \textbf{(and with complement)} \newline
$\Leftrightarrow True, \enspace  \therefore LHS \Rightarrow RHS$ is True, justifying the use of w-pre.


\subsubsection{Implication 8}
To prove the use of the \textbf{if1 rule} we need to prove that \newline
$[P \land (i != j) \land ((isPrime(i) \land isPrime(j)) \vee (\neg isPrime(i) \vee \neg isPrime(j))), \enspace P[\nicefrac{i+1}{i}]]$ \newline
implies \newline
$[(g \land \phi) \vee (\neg g \land \psi[\nicefrac{w}{w_0}], \enspace \psi]$, where
\begin{itemize}
    \item $\psi \enspace is \enspace P[\nicefrac{i+1}{i}]$, and
    \item $g \enspace is \enspace (isPrime(i) \land isPrime(j))$
\end{itemize}
POST-CONDITIONS:  $P[\nicefrac{i+1}{i}] \Rightarrow \psi$ is obviously true. \newline\\
PRE-CONDITIONS: Let $\psi \Leftrightarrow True$. \newline
$LHS \Rightarrow P \land (i != j) \land ((isPrime(i) \land isPrime(j) \vee \neg(isPrime(i) \land isPrime(j))$ \textbf{(De Morgan's law)} \newline
$\Rightarrow P \land (i != j) \land True$ \textbf{(And with complement)} \newline
$\Rightarrow P \land (i != j)$ \newline
$RHS \Rightarrow ((isPrime(i) \land isPrime(j)) \vee (\neg(isPrime(i) \land isPrime(j)) \land P[\nicefrac{i+1}{i}])$ \newline
$ \Rightarrow True \land P[\nicefrac{i+1}{i}]$ \newline
$\Rightarrow True$ since $P \Rightarrow P[\nicefrac{i+1}{i}]$ is true.



\subsubsection{Implication 9}
To use the \textbf{assignment rule}, we need to prove that $w = w_0$ which is true, and
$pre \Rightarrow post[\nicefrac{nEmirps + 1}{nEmpirps}]$, \newline\\
$RHS \Rightarrow (nEmirps + 1 \leq n) \land (i + 1 \geq 0)$ \newline
$\Rightarrow (nEmirps < n) \land (i > 0)$ \newline
Which is true when LHS is true since
\begin{itemize}
    \item $nEmirps \leq n \Rightarrow nEmirps < n$ is true, and
    \item $i \geq 0 \Rightarrow i > 0$ is true, by logic.
\end{itemize}
Hence justifying the use of the assignment rule.



   \section{Solution Questions}
   \subsection{Requirements}
   \subsubsection{Preconditions}
   \begin{itemize}
    \item  The given value $n$ is a natural number
   \end{itemize}
   \subsubsection{Postconditions}
   \begin{itemize}
    \item $i$ is the $n^{th}$ Emirp
    \item $Emirp(n)$ is defined as $n^{th}$ Emirp in the domain of $\mathbb{N}$ (natural numbers)
    \item $n$ is greater than or equal to 2
    \item The $n^{th}$ Emirp, $Emirp(n)$ is the $n^{th}$ prime number $i$, such that the reverse of $i$ is also a prime number
    \item $i$ is not a palindrome
    \item $Emirp(n)$ is between 2 and $N$
   \end{itemize}
   \subsubsection{Invariant}
   \begin{itemize}
    \item The variable $nEmirps$ is less than or equal to $n$
    \item The variable $i$ is greater than or equal to 2
   \end{itemize}


    \subsection{Formal Specification and Requirements}
    \subsubsection{Overall Specification}

    \begin{itemize}
        \item \(i:[ precondition  ,  postcondition  ]\)
        \begin{itemize}
            \item Here our specification is in the form of a program which stores the result in \(i\)
            \item The program \(E\) is such that once run with the preconditions, it should terminate successfully with a given postcondition.
        \end{itemize}

    \end{itemize}




    \subsubsection{Preconditions}

    \begin{itemize}
        \item \(n\in \mathbb{N}\)
        \begin{itemize}
            \item \(n\) is an element of the natural numbers.
            \item This therefore accounts for the fact that \(n\) must be greater than or equal to 0.
        \end{itemize}

    \end{itemize}



    \subsubsection{Postconditions}


    \begin{itemize}
        \item $i = Emirp(n)$
        \begin{itemize}
            \item This indicates that i is equal to the Emirp of $n$ which is also the $n^{th}$ Emirp
        \end{itemize}
        \item $Emirp(n) \in [2,n]$
        \begin{itemize}
            \item This indicates that the $n^{th}$ Emirp is between 2 and $N$
            \item This also indicates that $n$ is an element of $\mathbb{N}$, the natural numbers
        \end{itemize}
        \item $n \geqslant 2$
        \begin{itemize}
            \item This explains that $n$ must be greater than or equal to 2
            \item This therefore also indicates that 2 can not be considered an Emirp
        \end{itemize}
        \item $\forall i \in [2, N] \enspace \cdot \enspace (isPrime(i) \enspace \land \enspace isPrime(reverse(i)) \enspace \land \enspace (i \neq reverse(i))$
        \begin{itemize}
            \item This notes that the $i$ must be a prime number thna that its reverse, $reverse(i)$ must also be prime
            \item This part of the specification also mentions that $i$ can not be a palindrom since it is not equal to its own reverse
        \end{itemize}

    \end{itemize}

    \subsection{Changes in Translation to C Code}
    The changes we made in the translation from the derived code to the C program were minor:

    \begin{itemize}
          \item We added a main function to read in input from STDIN and print output to STDOUT.
          \item We declared the variables as unsigned long - this adds a limitation, restricting the size of the input number to the size of an unsigned long.
          \item Our of a reverse function changed - the one from our derived program was a function $reverse(n)$ which returns the reversed number, while the function $reversen(n, *r)$ takes in a pointer to the result.
          \item When proving $isPrime(n)$, we noticed a great inefficiency. When proving the its correctness, we found our specification continued to iterate through numbers from $i$ through $n$, even when the number was already classed as 'prime'.

    \end{itemize}


   \subsection{Tests - C Code}
   We tested our code on CSE servers and made runtime comparisons. This demonstrated the level of efficiency of our code:\\

   \noindent\textbf{Results}\\
   Input: 1 Time: 0.000s\\
   Input: 10 Time: 0.000s\\
   Input: 50 Time: 0.008s\\
   Input: 100 Time: 0.048s\\
   Input: 200 Time: 0.332s\\
   Input: 300 Time: 0.576s\\
   Input: 400 Time: 0.808s\\
   Input: 1000 Time: 11.769s\\
   Input: 2000 Time: 29.822s\\\\
   By running the program against a variety of inputs, the average runtimes can be seen. The program calculates the emirp by starting at 1 and incrementing until n emirps have been found, which demonstrates why the time increases quite rapidly as input size increases - the program has O(n) complexity.


\end{document}