Com S 641 Semantic Models for Programming Languages Homework: 8 Wim Hesselink. Programs, Recursion and Unbounded Choice. Cambridge, 1992. (Chapter 1) Recall our discussion about angelic and demonic choice. I'm not sure we really had either the right intuition about these commands, or that we came up with the right definitions for their wp and wlp. Since this is a good example of doing research, where problems aren't very clear cut, let's consider them again. I think the following description is better for the intuition. Informally angelic(c,d) always terminates if either c or d always does; angelic(c,d) has all the computations of c and d, but can loop forever only if both can loop forever. Informally, demonic(c,d) always terminates if both c and d always do; demonic(c,d) has all the computations of c and d, but cannot terminate when one must loop forever. Here's how you might execute these (i.e., a possible computation is...): angelic(c,d): run c and d in parallel (on copies of the state), use the state of the first one that terminates. demonic(c,d): run c and d until they both terminate (on copies of state), pick one final state. a. (extra credit only) Here is angelic(c,d) defined as a function from states to sets of states, where \bot means nontermination and c.x and d.x are the functions from states to sets of states for the commands c and d: angelic(c,d).x = { y | (~(y = \bot) /\ (y \in c.x \/ y \in d.x)) \/ (y = \bot /\ (\bot \in c.x /\ \bot \in d.x))} What would be a similar definition for demonic(c,d).x? b. It is clear from the informal definitions that wp.angelic(c,d).true = wp.c.true \/ wp.d.true wp.demonic(c,d).true = wp.c.true /\ wp.d.true Define wp.angelic(c,d), wp.demonic(c,d), wlp.angelic(c,d), and wlp.demonic(c,d) and say why your definitions seem "right" to you. c. Check that with your definitions in problem b: angelic(skip,abort) =~= skip demonic(skip,abort) =~= abort d. Is either angelic or demonic choice the same as the nondeterminate choice in Hesselink's book? (Chapter 2) This chapter starts with a more formal and abstract treatment of verification than we saw in Cohen's book. It then moves on to the treatment of procedures and recursive procedures. Loops are given a semantics by translation into recursion. The formal definition of the semantics and the soundness of the rules for recursion presented in this chapter will be discussed in chapter 4. (Section 2.1) e. Hesselink's exercise 2.1.0 (Section 2.2) f. Hesselink's 2.2.0 g. (extra credit; do Hesselink's 2.2.1) (Section 2.3) h. Hesselink's 2.3.1 i. Hesselink's 2.3.2 (Section 2.4) j. Do either Hesselink's exercise 2.4.0 or 2.4.1 (your choice). k. (extra credit) Do the exercise 2.4.0 or 2.4.1 that you didn't do for j. (Section 2.5) l. Hesselink's 2.5.0 m. (extra credit) Do one or more of Hesselink's other exercises for Section 2.5. (Section 2.6 and 2.7) n. Hesselink's 2.7.0 o. Hesselink's 2.7.1 p. (extra credit) Do one or both of Hesselink's 2.7.2 or 2.7.3. q. Hesselink's 2.7.4 (Section 2.8) r. Hesselink's 2.8.0 s. Hesselink's 2.8.1 t. Hesselink's 2.8.2 u. (extra credit) Do one or both of Hesselink's 2.8.3 or 2.8.4 v. (extra credit)Hesselink's 2.8.6