COMP2111 Assignment 3 2019 Term 1 Due: Monday 29th April, 23:59
Submission is through WebCMS/give and should be a single pdf file, maximum size 4Mb. Prose should be typed, not handwritten. Use of LATEX is encouraged, but not required.
Discussion of assignment material with others is permitted, but the work submitted must be your own in line with the University’s plagiarism policy.
Problem 1 (10 marks) The skip command is an L program that has the effect of “do nothing”. That is, skip; P has the same behaviour as P; skip and the same behaviour as P.
(a) Define skip using the default L commands – that is, write an L program for skip. (3 marks)
(b) Based on your definition and the rules of denotational semantics discussed in lectures, determine the
semantic object [[skip]]. (4 marks)
(c) Suppose skip was a default command in L. Propose a suitable rule for Hoare Logic that handles skip.
(3 marks)
Problem 2 (20 marks) Recall the diagonally-moving robot example from the lectures: from position (x, y) the robot can move to any of: (x+1,y+1), (x+1,y−1), (x−1,y+1), (x−1,y−1).
(a) Write a program in L+ that, on termination, will confirm that a location (m, n) is reachable by the robot starting at (0, 0). That is, the program Reach should be such that the Hoare triple
{(x = 0)∧(y = 0)}Reach{(x = m)∧(y = n)∧(m,n) is reachable from (0,0)} is valid, and the total correctness triple
[(x = 0)∧(y = 0)]Reach[(x = m)∧(y = n)]
is valid if and only if (m, n) is reachable from (0, 0). Note: your program does not have to terminate if
(m, n) is not reachable from (0, 0). (14 marks)
(b) Prove that your program is correct (i.e. show the validity of the partial correctness Hoare triple above). Annotating your code with appropriate assertions, as long as the proof is recoverable, is sufficient.
(6 marks)
Problem 3 (10 marks) Suppose you have ten coins arranged in a line. A move consists of taking any three adjacent coins and turning them over (changing heads to tails and vice-versa). For example, if the coins were arranged as:
HHTTHTHTHT
1
one move could be to flip the second, third and fourth coins to get the arrangement:
HTHHHTHTHT
(a) Model this situation as a transition system, carefully defining your states and the transition relation. (4 marks)
(b) By considering the coins in positions 1,2,4,5,7,8, and 10 (i.e. positions not divisible by 3) find a pre- served invariant of this system. (4 marks)
(c) Show that the arrangement TTTTTTTTTT is not reachable from the arrangement HHHHHHHHHH. (2 marks)
Problem 4 (10 marks) Let Σ = {0,1}3, so each element of Σ is a triple of symbols that are either 0 or 1. Let f,s,t : Σ∗ → {0,1}∗ be the functions that take a word from Σ∗ and return the word of {0, 1}∗ that is defined by considering
0101 only the symbols in the first, second, or third (respectively) component. So if w = 0 1 1 0 ,
0010 then f (w) = 0110, s(w) = 0101 and t(w) = 0010. Finally, let bin : {0, 1}∗ → N be the function that treats a word of {0, 1}∗ as the binary representation of a non-negative integer, with the last symbol being the
least-significant. So bin(110) = bin(00110) = 6 and bin(λ) = 0. Design a DFA that accepts the following language:
{w ∈ Σ∗ : bin(t(w)) = bin( f (w)) + bin(s(w))}.
Problem 5
Let L ⊆ Σ∗ be a language over Σ. Recall the definition of ≡L⊆ Σ∗ × Σ∗:
w≡L v iff ∀z∈Σ∗ :wz∈L⇔vz∈L (a) Show that ≡L is an equivalence relation.
(10 marks) (10 marks)
(6 marks)
(b) If L is regular, show that for any word w, [w] (the equivalence class of w under ≡L) is also regular.
(4 marks)
2