# 编程代写 | COMP3610/6361 Principles of Programming Languages Assignment 4

## 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]

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 !i <!n do (
i :=!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.

### 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

od

Is the above program terminating? An informal argument, using e.g. the transition system, is sufﬁcient.

## 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.