I. Predicate Transformers (Chapter 11) A. satisfying contracts (11.1) ------------------------------------------ SATISFYING CONTRACTS (11.1) Language of contracts S ::= | {g} | [g] | S1 \join S2 | S1 \meet S2 | S1;S2 Let s be a state, q a predicate. When should s {| S |} q hold for these? ------------------------------------------ When is s {| |} (x == 3) ? When is s {| |} (x == 3) ? When is s {| |} (x >= 3) ? When is s {| {x >= 3} |} (x >= 3) ? When is s {| {x >= 3} |} (x >= 4) ? When is s {| {x >= 4} |} (x >= 3) ? When is s {| [x >= 4] |} (x >= 3) ? When is s {| [x >= 3] |} (x >= 4) ? When is s {| [x >= 3]; |} (x >= 4) ? When is s {| {x >= 3}; |} (x >= 4) ? When is s {| {x >= 3} \join |} (x >= 4) ? When is s {| [x >= 3] \join |} (x >= 4) ? When is s {| {x >= 3} \meet |} (x >= 4) ? When is s {| [x >= 3] \meet |} (x >= 4) ? What sets do these define? B. weakest preconditions ------------------------------------------ WEAKEST PRECONDITIONS Definition: let S be a contract, and let q be a predicate. Then the weakest precondition following S to establish q, wp.S.q is ^ wp.S.q = {s | s {| S |} q} wp.S is a predicate transformer, since wp: P(\Sigma) -> P(\Sigma) wp..q == f^{-1}.q wp.{g}.q == g \intersect q wp.[g].q == !g \union q wp.(S1 \join S2).q == wp.S1.q \/ wp.S2.q wp.(S1 \meet S2).q == wp.S1.q /\ wp.S2.q wp.(S1 ; S2).q == wp.S1.(wp.S2.q) ------------------------------------------ In what sense is this the weakest? How would you express s {| S |} q using wp? What is wp..(x == 3) ? What is wp..(x == 3) ? What is wp..(x >= 3) ? What is wp.{x >= 3}.(x >= 3) ? What is wp.{x >= 3}.(x >= 4) ? What is wp.{x >= 4}.(x >= 3) ? What is wp.[x >= 4].(x >= 3) ? What is wp.[x >= 3].(x >= 4) ? What is wp.([x >= 3]; ).(x >= 4) ? What is wp.({x >= 3}; ).(x >= 4) ? What is wp.({x >= 3} \join ).(x >= 4) ? What is wp.([x >= 3] \join ).(x >= 4) ? What is wp.({x >= 3} \meet ).(x >= 4) ? What is wp.([x >= 3] \meet ).(x >= 4) ? C. Predicate Transformers (11.2) ------------------------------------------ PREDICATE TRANSFORMERS (11.2) Definition: The set of *predicate transformers* from S to G is ^ (S |-> G) = P(G) -> P(S) . Examples: wp.skip wp.begin wp.(x := x+1) wlp.(x := x+1) ------------------------------------------ Why is the map backwards like that, starting with P(G)? 1. predicate transformer lattice ------------------------------------------ PREDICATE TRANSFORMER LATTICE Definition: Let wg.C1, wg.C2 \in S |-> G. Then ^ wg.C1 \refinedby wg.C2 = (\forall q \in P(G) :: wg.C1.q \subseteq wg.C2.q) ------------------------------------------ Is (S |-> G, \refinedby) a lattice? Complete? Boolean? ------------------------------------------ LATTICE CONSTANTS AND OPERATIONS abort.q == false (\bot of p.t.) magic.q == true (\top of p.t.) (!(wg.C)).q == !(wg.C.q) (! of p.t.) (wg.C1 \meet wg.C2).q == (\meet of p.t.) wg.C1.q \intersect wg.C2.q (wg.C1 \join wg.C2).q == (\join of p.t.) wg.C1.q \union wg.C2.q ------------------------------------------ So what is (!wp.(x := 3)).(x == 3) ? What is wp.({x == 3}; x := x+1) \join wp.(x := x) ? What is wp.(x := x+1) \join wp.skip ? What is wp.(x := x+1) \meet wp.skip ? What is wp.(x := x+1) \join wp.(x := x+2) ? What is wp.(x := x+1) \meet wp.(x := x+2) ? How would you define implication and equivalence of predicate transformers? Is there any difference between implication of predicate transformers and refinement? What other operations would we want on a complete lattice? 2. predicate transformer category ------------------------------------------ PREDICATE TRANSFORMER CATEGORY Definition: a predicate transformer category has types as objects and predicate transformers as morphisms. 1 == skip (1 of p.t.) wg.C1; wg.C2 == wg.C1 o wg.C2 (; of p.t.) E.g., Ptran_X(S,G) == S |-> G where S, G \in X ------------------------------------------ Why is composition backwards function composition? what are the properties that the unit must satisfy? why is composition associative? What does it mean for a predicate transformer to be monotonic? Is wp.skip monotonic? wp.(x := e)? wp.[false]? Is composition monotonic? ------------------------------------------ DISTRIBUTIVITY LAWS From the right also for lattic operations: magic; T == magic abort; T == abort (!S); T == !(S;T) (S1 \meet S2); T == (S1;T) \meet (S2;T) (S1 \join S2); T == (S1;T) \join (S2;T) ------------------------------------------ How would you generalize these last two? II. Basic Predicate Transformers (Chapter 11.3) ------------------------------------------ PREDICATE TRANSFORMER SUGARS .q == f^{-1}.q (functional update) {g}.q == g \intersect q (assertion) [g].q == !g \union q (assumption) So... abort == {false} skip == == {true} == [true] magic == [false] ------------------------------------------ With this notation, what is wp.? wp.skip? Why is abort called that? What is the intuition behind "magic"? ------------------------------------------ ASSIGNMENT STATEMENTS The most useful functional update .q.s == { definition } q((x := e).s) == { substitution theorem } q[x := e].s Thm 11.2: Let x be an (list of) attribute(s), let e be an (list of) expression(s), and let q be a Boolean expression. Then var x |- .q == q[x := e] ------------------------------------------ Can you simplify (;).(x > y) ? III. Relational Updates (11.4) Intuitively, what is does an angelic update, {R}, based on relation R do? What does a demonic update, [R], based on relation R do? ------------------------------------------ RELATIONAL UPDATES Definitions: {R}.q.s == (\exists g :: R.s.g /\ q.g) [R].q.s == (\forall g :: R.s.g ==> q.g) Sugars wp.{R} == {R} wp.[R] == [R] Special cases: choose == {True} (arbitrary choice) chaos == [True] (chaotic choice) ------------------------------------------ How does that match intiution? How would you describe these in terms of set notation? What is {False}? [False]? ------------------------------------------ RELATIONAL ASSIGNMENTS Demonic: [x := x' | b] Angelic: {x := x' | b} Theorem 11.3. Assume that x is a list of program variables and b is Boolean expression, and q is a Boolean expression in which x' does not occur free. Then (a) var x |- {x := x' | b}.q == (\exists x' :: b /\ q[x := x']) (b) var x |- [x := x' | b].q == (\forall x' :: b ==> q[x := x']) ------------------------------------------ What is [x := x' | x' > x + y].(x > y)? What is [x := x' | x' > x + y].q? What is [x := x' | x * x <= x' /\ x' < (x+1)*(x+1)].(x == 2)? IV. Duality (11.5) ------------------------------------------ DUAL OF A PREDICATE TRANSFORMER Definition S^{o}.q == !S.(!q) (dual pred. trans.) Theorem 11.4. The following dualities hold between predicate transformers: ^{o} == {p}^{o} == [p] {R}^{o} == [R] (S1;S2)^{o} == S1^{o};S2^{o} (\join i \in i :: S.i)^{o} == (\meet i \in i :: S.i^{o}) ------------------------------------------ What is the dual of the dual of a predicate transformer? What is [p]^{o}? [R]^{o}? magic^{o}? abort^{o}? skip^{o}? V. Preconditions and Guards (11.6) ------------------------------------------ PRECONDITIONS AND GUARDS Definition: Let wg.C : S |-> G. Then m, t: (S |-> G) -> P(S) are defined by miracle precondition: m.(wg.C) == (\intersect q \in P(G) :: wg.C.q) abortion guard: t.(wg.C) == (\union q \in P(G) :: wg.C.q) abortion precondition: a.(wg.C) == !t.(wg.C) miracle guard: g.(wg.C) == !m.(wg.C) ------------------------------------------ What do these mean intuitively? Why is m.(wg.C) \subseteq t.(wg.C)?