Appendix B. Exercises

Table of Contents

Operational semantics
Denotational semantics
Partial correctness in Hoare logic
Total correctness of while programs
The wp-calculus
Recursive programs

Operational semantics

We illustrate the methods presented in the previous sections through some solved exercises.

Exercise 1. Let . Let . Present at least five steps of the computation in the operational semantics starting from the configuration . In the second member of the configurations below, the tuples stand for the values , and , in this order.

Solution.

where

Exercise 2. Let be the factorial program as in the previous exercise. Construct the set in the style of Definition 12. We preserve the notation of the previous exercise concerning the subparts of program C.

Solution.

Exercise 3. Construct a computational (transitional) sequence for C in Exercise 1 starting from making use of the operational semantics defined in the previous exercise.

Solution.

Exercise 4. Let . Let , assume , . Present a computation in the operational semantics starting from the configuration . In the second member of the configurations below, the tuples stand for the values , , in this order.

Solution.

where

Exercise 5. Let C be as in Exercise 4. Let us keep the notation for the labels of C of the above exercise. Formulate the operational semantics of C on the pattern of 12. Let and as before.

Solution.

Exercise 6. Construct a computational (transitional) sequence for C, if C is as in Exercise 4, starting from making use of the operational semantics defined in the previous exercise. Assume and .

Solution.