COMP3151/9154 Homework 6

Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: daixieit

COMP3151/9154

Homework (Week 7)

Due: 9am Mon 17 July 2023

1. Non-compositional Verification: Here is a three process message pass- ing system presented as a transition diagram of three processes P1 , P2 , and P3 .

Prove using the Levin and Gries or AFR methods that the following Hoare triple holds:

{True} P1   ∥ P2   ∥ P3  {y = v − 1}

Give your assertion networks, your extra auxiliary variables, and (if us- ing AFR) your communication invariant.   List and discharge the proof obligations.

2. Termination: Consider the following program:

(a)  Use the local method to prove x ≥ 0 -convergence for this program. You’ll need exit locations for p and q (not shown in the above pseu- docode). First specify your assertion networks, your wellfounded set, and your ranking functions.  Then list and discharge the proof obli- gations.

(b) Is this program 」-convergent? Briefly motivate your answer. (c) Is this program T-convergent? Briefly motivate your answer.

You may assume that the x := x — 1 and x := 2（x are executed atomically.