© P. Ho¨fner
COMP3610/6361 Principles of Programming Languages
Assignment 4
ver 1.0
Submission Guidelines
• Due time: Nov 2, 2023, 11am (Canberra Time)
• Submit a pdf via Wattle.
• Scans of hand-written text are fine, as long as they are readable and neat.
• Please read and sign the declaration on the last page and attach a copy to your submission.
• No late submission, deadline is strict
Exercise 1 (Hoare Logic) (35 Marks)
Question 1 Prove the total correctness for the following Hoare triple
[x≤ n] while !x< !n do x := !x+1 [x= n]
To prove total correctness, first prove partial correctness. Then give a (formal) argument why the while-
loop terminate. For example, you can provide a function that decreases whenever the while loop is
executed. Explain all steps; in particular clearly identify the invariant of the while-loop.
Question 2 Consider the following Hoare triple (partial correctness)
{n≥ 0}
i := 0 ;
x := 0 ;
y := 0 ;
z := 1 ;
while !ii := !i+1 ;
x := !x+ !y+ !z ;
y := !y+ !z+ !z+1 ;
z := !z+3)
{x= n3}
• Give an invariant for the while-loop. Explain why the invariant is derivable from the precondi-
tion(s); no formal proof needed.
• Decorate the program with pre- and postconditions, as shown in the lecture. The decorations are
enough, no formal derivation needed.
2 COMP3610/6361
Question 3 Calculate the weakest liberal preconditions for the following programs and postconditions.
• wlp(x := !x+ !y, x= y+ y)
• wlp(while y> 0 do y := !y−2, even(y))
(As invariant you can use even(y).)
Exercise 2 (Guarded Command Language) (15 Marks)
Consider the following program in GCL over variables x and y whose domains are the integers Z (int).
do
x> y→
if
x− y≤ 5→ y := y−1
[]
x≤ 0→ x := x−1
fi
od
Is the above program terminating? An informal argument, using e.g. the transition system, is sufficient.
Exercise 3 ((Pure) CCS) (30 Marks)
Consider a vending machine that accept pieces of 20 cents, 50 cents and 1 dollar, and that can dispense
chocolate and pretzels, each of which costs 1 dollar.
Question 4 Create a CCS process describing the vending machine. The set of actions should include
‘20c’, ‘50c’ and ‘1$’ , indicating the reception by the machine of a coin inserted by a user. The set should
also include actions ‘chocolate’ or ‘pretzel’, indicating the opening of the glass door of the machine
behind which chocolate or pretzels are stored.
We abstract from the closing of the door after extraction of the pretzel, which happens automatically,
and the appearance of a new pretzel behind the glass door afterwards. Assume that the machine does not
give change, and that it accepts any amount of surplus money. Try to make the CCS expression as short
as possible.
Question 5 Give a process graph (labelled transition system) that correspond to your CCS process.
Exercise 4 ((Pure) CCS & Semantic Equivalences) (20 Marks)
Question 6 For which possible choices of Q and R are there transitions of the form
a.(c¯+b)∥ ((c+ a¯)∥ b¯) τ−→ Q τ−→ R
in the labelled transition system of CCS? Explain your answer; in particular discuss why there cannot be
more Q’s and R’s not listed as part of your answer. Give a proof tree of the formal derivation of one of
those transitions from the structural operational rules of CCS.
P. Ho¨fner 3
Academic Integrity
I declare that this work upholds the principles of academic integrity, as defined in the University Aca-
demic Misconduct Rule; is entirely my own work, with only the exceptions listed; is produced for the
purposes of this assessment task and has not been submitted for assessment in any other context, except
where authorised in writing by the course convener; gives appropriate acknowledgement of the ideas,
scholarship and intellectual property of others insofar as these have been used; in no part involves copy-
ing, cheating, collusion, fabrication, plagiarism or recycling.
Date Signature