CSC3001 Formal Methods
Alternative Assessment 2020/21

Please read the following information carefully.

Thursday 13th May 2021 10.00 – 13.00 + 1 hour
(If you receive extra time please see email correspondence for confirmation of your
specific timing arrangements)

Updates to the class (if necessary) regarding the exam paper will be posted on Canvas
announcements and email so students should periodically check Canvas or their email during
the assessment and ensure Canvas announcements are on.

Normal University regulations relating to academic offenses, including
collusion and plagiarism apply

All questions carry equal marks
Answer any FOUR Questions

 The use of Overture tool and a calculator is permitted.
 Solutions should be completed electronically or using pen and paper.
 If you are completing your solutions on pen and paper you may wish to use Microsoft
Lens to collate your solutions in to a single PDF file to aid submission. A short
instructional video is available here: https://youtu.be/n2AfsZxuVMk
 You should write your student number clearly on the top of each page.
 Solutions should be submitted through the assignment page for this assessment.
 By submitting the work, I declare that:
1. I have read and understood the University regulations relating to academic
offences, including collusion and plagiarism:
http://www.qub.ac.uk/directorates/AcademicStudentAffairs/AcademicAffairs/Gener
alRegulations/Procedures/ProceduresforDealingwithAcademicOffences/
2. The submission is my own original work and no part of it has been submitted for any
other assignments, except as otherwise permitted;
3. All sources used, published or unpublished, have been acknowledged;
4. I give my consent for the work to be scanned using a plagiarism detection software.
 If you require clarity on questions please email Dr Gault (richard.gault@qub.ac.uk).
Examiners: Dr Richard Gault
Dr Amir Sabbagh Molahosseini
Prof. F Moller
and the internal examiners
CSC3001/2021-Main
1. Data Types
A greyscale image can be represented as a mapping where every pixel, referenced by a row
and a column, maps to a value between 0 and 255 that represents the brightness of the
pixel. Typically 0 corresponds to black and 255 corresponds to white. For example, given the
greyscale image in Figure 1
Figure 1: Example greyscale image
the pixel in the second row of the first column would be represented by {mk_(2,1)|−>200}.
(a) (i) Using map enumeration define the mapping for the 4 pixel greyscale image shown
in Figure 1. [2 marks]
(ii) Illustrate with a diagram similar to the greyscale image shown in Figure 1, the greyscale
image defined by the following mapping
{mk_(1,1)|−>127,mk_(1,2)|−>100,mk_(2,1)|−>255,mk_(2,2)|−>50}
[1 mark]
(iii) Similar to Q1(a)(ii), illustrate the greyscale image defined by the following mapping
{mk_(a,b)|−>c|a,b in set {1,2,3}, c in set {0,1} & if a==b then c= 1 else c = 0}
[2 marks]
(b) (i) Given that an image must be exactly 600 pixels tall (i.e. rows) and 800 pixels wide
(i.e. columns) define two data types, rows and cols, that are sets containing the ap-
propriate row and column indices. Note that the top left pixel in any greyscale image
will be referenced as (1,1). [3 marks]
(ii) Using your answer to Q1(b)(i), or otherwise, define the datatype “greyImage" to rep-
resent a greyscale image using map comprehension. [2 marks]
(c) In image processing a “binary threshold” is a simple filter that can be applied to a given
image. This filter will set any pixel above or equal to the specified threshold to be 1 and
all other pixel values to be 0. Complete the following function definition to compute the
binary threshold of a given image to a given threshold value.
binThreshold: greyImage ∗ {0,...,255} −> greyImage
binThreshold(g,threshold)== ... [4 marks]
[continued overleaf]
CSC3001/2021-Main
(d) Image augmentation is a common practice in machine learning investigations and is used
to increase the number of data samples by adjusting the existing images to create new
images. Two common augmentations are mirroring and flipping. In mirroring the image
is horizontally reflected around the mid point of the image whilst in flipping the image is
vertically reflected around the mid point. Figure 2 illustrates both these processes applied
to a single image in a scaled down example.
Figure 2: Example augmentation applied to the original image X
Provide function definitions for the augmentations mirror and flip. [6 marks]
CSC3001/2021-Main
2. Specification
(a) A Database can be considered as a set of elements where each element is a non-empty
sequence of characters.
(i) Explain why a set would be a sensible datatype to model a database. [1 mark]
(ii) Specify the datatypes Element and Database as described above. [2 marks]
(iii) Given the following specification details
state S of
dB:Database
end;
provide a specification for the following operations
• initialise: which should set the state to be empty
• addElement: which should add a new element in to the database
• findElement: which should return whether a specified element is contained in the
database.
[7 marks]
(b) A shop stocks milk on their shelves with at most 5 products in a row along the front of the
shelf and at most 10 rows of product deep on the shelf which would fill the shelf.
(i) Complete the following type definitions, including any necessary invariants, to show
how sequences can be used to model the milk stock in each row and all the rows on
the shelf. You may assume the existence of a data type Milk.
row = ...
shelf = ...
state S of
m:shelf
end;
[2 marks]
Give implicit specifications of the following operations which modify the global state
m:shelf. Remember to include any necessary pre-conditions.
(ii) removeStock(n:nat1) which removes the front n rows of stock and brings forward the
stock in the back of the shelf towards the front of the shelf. [2 marks]
(iii) rotateStock(s:nat1, f:nat1,p:nat1) which moves a block of stock that starts at row s
and finishes at line f (inclusive) so that it is placed immediately before row p. The pre-
condition must guarantee that p does not lie within the block of stock to be moved.
Hint: Consider separately the cases pf.
Explain how your specification for rotateStock does not affect the total number of
rows on the shelf. [6 marks]
CSC3001/2021-Main
3. Recursive Data Types
A sorted binary tree is a binary tree where all children to the left of a particular node are less
than the value of the node and all children to the right of a particular node are greater than the
value of the node.
(a) Complete the invariant for the datatype SNode shown below
SNode::v:nat
l:SBinTree
r:SBinTree
inv mk_SNode(v,l,r)== ...
SBinTree[SNode]
Note that you can assume the existence of a function vals:SBinTree −>set of nat which
returns all values contained within a given SBinTree. [2 marks]
(b) Provide a recursive definition for the function insert which inserts a given value in to a
given SBinTree if the value is not already in the tree. If the value is already in the given
SBinTree then the original SBinTree should be returned. [3 marks]
(c) The height of a SBinTree is the longest path between the root node and any non-nil leaf
node (inclusive of both the root and leaf node). For example, the height of the SBinTree
shown in Figure 3 is 3 which has the longest path highlighted.
Figure 3: Example of a sorted binary tree of height 3.
Define a recursive function “height" that returns the height of a given SBinTree.
Note you may assume the existence of a function “greater" which returns the larger of 2
given natural numbers. [3 marks]
(d) Suggest an induction rule for SBinTree. [2 marks]
(e) Define a recursive function countVals to return the number of non-nil elements within a
given SBinTree. [2 marks]
[continued overleaf]
CSC3001/2021-Main
(f) Using your induction rule from Q3(d) and your definitions of height and countVals prove
that
forall T:SBinTree & countVals(T)<2∗∗(height(T)).
[8 marks]
CSC3001/2021-Main
4. Refinement
Assuming that the types Name and Address are available, an address book can be defined
by:
AddressBook::friends: set of Name
address: map Name to Address
sendcard: set of Name
inv mk_AddressBook(f,a,s)==dom a = f and s subset f;
The purpose of field sendcard is to record those people to whom holiday postcards are to be
sent.
(a) (i) Briefly justify the invariant which has been given for the type AddressBook. [2 marks]
(ii) Define an inference rule for membership of the type AddressBook. [1 mark]
(b) Consider the following operation:
add(n:Name,a:Address)
ext wr ab:AddressBook
pre not n in set ab.friends
post ab = mu(ab~, friends |−> ab~.friends union {n},
address|−>ab~.address munion {n|−>a})
(i) Explain why munion can be utilised specifically in the post condition of add without
concern of an error arising. [2 marks]
(ii) Specify an operation tidy which removes from an address book those friends to
whom cards are not sent. [2 marks]
(c) The type AddressBook can be refined to the concrete type AddressBookC:
AddressBookC::friends: seq of Name
address: seq of Address
sendcard: seq of bool
inv mk_AddressBookC(f,a,s)== ...;
(i) Suggest an invariant for the type AddressBookC. [3 marks]
(ii) Refine the operations add and tidy in part (b) to operations addC and tidyC which
act on a value of type AddressBookC. [5 marks]
(d) State and then prove the implementability requirement for the operation addC. [5 marks]
CSC3001/2021-Main
5. Recursive Equations and Axiomatic Semantics
(a) Consider the recursive function
f:nat1−>nat1
f(x)== if x = 1 then 1 else x∗x +f(x−1)
(i) Use the definition of f to evaluate f(1), f(2), f(3), f(4). [2 marks]
(ii) Define a functional representation, T, of the function f. [1 mark]
(iii) Define a chain of functions f0(x)= Ω, f1(x)= T(f0,x), f2(x) = T(f1,x) and f3(x) = T(f2,x).
Suggest a defintion for the general form of the function fi = T(f{i−1},x). [3 marks]
(iv) Prove by induction that your hypothesised definition of fi holds for all i:nat. [5 marks]
(b) Consider the following specification:
factorChecker(a:nat)r:bool
ext rd b:nat
pre a<=b and a>1
post r <=>b~ mod a <>0
Consider the following program fragment. All variables are of type nat with the exception
of the variable r which is of type bool.
n = 0;
while (b>=a)
{
b = b−a;
n = n+1;
}
r = (b >0);
(i) Copy and complete the table below to show how each variable develops on each
iteration of the loop assuming that initially b = 10 and a = 3.
iteration n b~ a b b>=a
0 0 10 3 10 True
[1 mark]
(ii) Suggest a loop invariant and prove that the code fragment is partially correct with
respect to the operation factorChecker. [8 marks]
CSC3001/2021-Main
6. Specification
(a) (i) Consider the types
T1 = map nat to nat
T2 = map nat to nat | bool
T3 = map nat | bool to nat | bool
T4 = map bool to nat | bool
To which of these types (if any) do the following belong:
• {1|−>2, 2|−>1}
• {1|−>true, true|−>1}
• {true|−>1, false|−>0}
[3 marks]
(b) A supermarket requires a stock management system to record details of the products
which it sells and the levels of stock. Each project is identified by a unique numeric value.
The system uses maps to store information about its products. For each project there is
a description (sequence of characters), price (in pence) and stock level (whole number).
The numeric keys in the domain of the System should satisfy that every numeric key
from 1 to maximum key value should be used (i.e. no numeric value between 1 to the
maximum key value is missing).
(i) Assuming the existence of a function max:set of nat1 −> nat1 that returns the max-
imum value in a given set, complete the following VDM-SL description:
Product :: description : ...
price : ...
stock : ...
System = map nat1 to Product
inv(s) == ...;
state S of
sys:System
end;
[2 marks]
(ii) Specify the operation sell(i:nat1, x:nat1) on System which indicates that the super-
market has sold x instances of the ith item in the system. [2 marks]
(iii) Specify the operation discount(count:nat1, n:nat1) on System which will reduce by
n percent the price of all products which are in surplus (rounded down to the nearest
penny). That is, those products for which the stock level is greater than count.
Hint: Consider using an if - then - else expression to specify the difference between
the components of the state that are changed and separately those items that are
unchanged.
[4 marks]
[continued overleaf]
CSC3001/2021-Main
(c) It is possible to represent the system mapping outlined in Q6(b) by a sequence, where
each domain element becomes the index of the corresponding Product in the sequence
of all products.
(i) Using this technique of representing maps as a sequence, produce a reification
SystemC of the record System from Q6 (b). You should include an appropriate
retrieve function and refine the operation sell to sellC that provides an equivalent
operation on SystemC. [5 marks]
(ii) Prove the adequacy of your retrieve function defined in Q6(c)(i).
[4 marks]