本次澳洲代写是Principles of Programming Languages的一个assignment

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