Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- \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*}
- E : [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 (Mod(X, i) \neq 0)
- \end{equation*}
- \begin{equation*}
- Mod(X, Y) = X - (X-Y)
- \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
- $E : [n \in \mathbb{N} , \enspace Emirp(n)]$ \newline\\
- $\sqsubseteq \enspace var\enspace nEmirps : \mathbb{N} \enspace \cdot \enspace \textcolor{red}{\llcorner} E, nEmirps : [n \in \mathbb{N}, \enspace Emirp(n)] \textcolor{red}{\lrcorner} $ \textbf{(i-loc rule)} \newline
- $\textcolor{red}{\sqsubseteq} \enspace var \enspace i : \mathbb{N} \enspace \cdot \enspace \textcolor{orange}{\llcorner} E, i, nEmirps : [n \in \mathbb{N}, \enspace Emirp(n)] \textcolor{orange}{\lrcorner} $ \textbf{(i-loc rule)} \newline
- $\textcolor{orange}{\sqsubseteq} \enspace \textcolor{blue}{\llcorner} E, i, nEmirps : [n \in \mathbb{N}, \enspace P] \textcolor{blue}{\lrcorner}
- \enspace \textbf{;} \enspace \textcolor{green}{\llcorner} E, i, nEmirps :[P, \enspace Emirp(n)] \textcolor{green}{\lrcorner}$ \textbf{(seq)} \newline
- $ \textcolor{blue}{\sqsubseteq} \enspace E, i, nEmirps : [n \in \mathbb{N}, \enspace P[\nicefrac{0}{nEmirps}]] \enspace \textbf{;} \enspace
- E, i, nEmirps [P[\nicefrac{0}{nEmirps}], \enspace P] $ \textbf{(seq)} \newline
- $\sqsubseteq \enspace nEmirps := 0\enspace ; \enspace E, 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} E, 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} E, i, j, nEmirps:[(nEmirps < n) \land P, \enspace P] \textcolor{green}{\lrcorner} $ \textbf{(i-loc)} \newline
- $\textcolor{green}{\sqsubseteq} \enspace E, i, j, nEmirps : [(nEmirps < n) \land P, \enspace P \land ((i != j) \vee (i = j))] \enspace \textbf{;} \newline
- \indent \indent \indent E, 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} E, 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 E, i, j, nEmirps : [P \land (i = j \vee i != j), \enspace P[\nicefrac{i+1}{i}]] \enspace \textbf{;} \newline
- \indent \indent \indent E, i, j, nEmirps : [P[\nicefrac{i+1}{i}], \enspace P] $ \textbf{(seq)} \newline
- $\sqsubseteq \textcolor{green}{\llcorner} E, 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} E, 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 E, 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} E, 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 \(E:[ precondition , postcondition ]\)
- \begin{itemize}
- \item Here our specification is in the form of a program, given by \(E\)
- \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 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 naumber 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}
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement