Q$6$ Specification $[15]$ Consider an array $a$ of Boolean values of

size $n,$ where $n$ is a multiple of $8.$ Here, we will treat true as $1$ and

false as $0.$

We want to create a specification to indicate that the output array

of Booleans $b$ is larger than $a,$ such that after every $8$th element of

array $a$ an even parity element is inserted. Recall that even parity

counts the number of ones in a byte. If there is an even number

of ones, the parity bit is $0$ ; if there is an odd number of ones, the

parity bit is $1.$ You must write a formal behavioural specification

that captures all of the above information. Remember that among

other things you will need to:

Define the signature.

Specify the exact size of the output array.

Describe how the parity bit must be calculated.

Q$7$ Implementing Specifications $[20]$

$($a$)$ Given $=\{x|R,y|R,z|R\},$ implement $($using

forward substitution$)$ the following specification using a sequence

of $($nonparallel$)$ assignments. $[10$ marks$]$

$($:$(x^{\text{'}},y^{\text{'}})=(x{m}^2+x+my,y+mx)$:$)$

$($b$)$ Use the alternation law to implement the following. $[10$ marks$]$

$($:$\{x^{\text{'}},y^{\text{'}},z^{\text{'}}\}=\{x,y,z{\}}^{{?}^{?}}{x}^{\text{'}}{y}^{\text{'}}{z}^{\text{'}}$:$)$