I. Overview (Back and von Wright, Ch 1) ------------------------------------------ MAIN QUESTIONS (Ch. 1) Problems: - Is a program correct, with respect to a specification? - How can we improve a program, while preserving correctness? Idea: - Programs and specifications are the same thing -- contracts between agents ------------------------------------------ ------------------------------------------ MATHEMATICAL BASIS Higher-order logic Lattice theory Notation: A -> B A -> B -> C f.x f.a.b ------------------------------------------ A. contracts (1.1) 1. states what are states (\sigma) used for? What are they made of? 2. state space what is a state space (\Sigma)? What are the operations on states? 3. functional update how does an agent update the state? how do we model assignments? 4. a language of contracts what's the purpose of a contract? what's the simplest language we could have for contracts? ------------------------------------------ SIMPLE CONTRACTS S ::= "contract" "basic action" | S1 ; S2 "sequencing" | S1 \join S2 "alternative (free choice)" assume that ";" binds more strongly than "\join" Note that \join is the LaTeX \sqcup symbol ------------------------------------------ how would you define a contract that does nothing to the state? how would you define a contract that multiplies x by y? that can either multiplies x by y or does nothing? can an agent following this contract change the value of z? does the state space have to have attributes x and y for this to make sense? how would you define when an agent satisfies a contract? why is S1; (S2; S3) == (S1; S2); S3? why is S1 \join (S2 \join S3) == (S1 \join S2) \join S3? is S1;S2 == S2;S1? is S1 \join S2 == S2 \join S1? 5. cooperation between agents how do the authors model a contract that specifies cooperation between two independent agents? how would you specify a contract for me printing a file? is our language really expressive enough for multiagent contracts? if not, what's missing? a. assertions how can an agent satisfy an assertion? Not satisfy it? What assertion is always breached? satisfied? How can we assign blame in a two party contract? How does this relate to games? b. assumptions how does an assumption relate to a precondition? what happens if an assumption isn't satisfied? is this realistic in real-life contracts? B. Using contracts (1.2) 1. Taking sides ------------------------------------------ TAKING SIDES (1.2) S ::= "contract" "basic action" | S1 ; S2 "sequencing" | S1 \join S2 "our choice" | S1 \join^o S2 "other agent's choice" | { g } "our assertion" | { g }^o "other's assertion" | [ g ] "our assumption" | { g }^o "other's assumption" Examples [ x > 0]; z := y - x; { z < y } [ x > 0]^o; z := y - x; { z < y }^o ------------------------------------------ in which of these is our agent the server? which one most matches the normal kind of specification of a procedure? What's the other one about? What's the meaning of { x > y }? What's the meaning of [ x > y ]? If a contract is a game, when can our agent win? What if the other agent breaches the contract? 2. generalizing to multiple agents how can we generalize this to multiple agents? 3. contracts as games if we think of this as a game, what expresses the game's rules? what does it mean if the angels have a winning strategy? how can a demon lose? does somebody always win this game? C. computers as agents (1.3) what are these agents? can computers really make choices? when we are programming the client, can the server's choices be bad for us? How about vice versa? D. algebra of contracts (1.4) how would you compare two contracts from the point of view of our agent? ------------------------------------------ REFINEMENT (BIGGER IS BETTER) def: A contract S is refined by S' iff for all states \sigma, for all predicates q, \sigma {| S |} q ==> \sigma {| S' |} q We write S \refby S' for this, where \refby is LaTeX's \sqsubseteq symbol ------------------------------------------ Which is the better contract? what does this have to do with Texas? is refinement reflexive? Transitive? Symmetric? Antisymmetric? so what kind of ordering is it? what's the best possible contract from our agent's point of view? the worst? so what's the least element in the contract ordering? the greatest? ------------------------------------------ EXAMPLES Consider: (a) x := x + 1 \join x := x + 2 (b) x := x + 1 (c) x := x + 2 Which refine the others? What about: (d) x := x + 1 \join^o x := x + 2 ------------------------------------------ ------------------------------------------ LATTICE PROPERTIES When is the following true? s {| x := x + 1 \join x := x + 2 |} q E.g., do the following hold? why? (x|->0){|x := x + 1 \join x := x + 2|} x==1 (x|->0){|x := x + 1 \join x := x + 2|} x==2 What if \join is replaced by \join^o? ------------------------------------------ E. programming constructs (1.5) How would you define abort? Skip? 1. conditional contracts how can we define it-then-else in terms of our current syntax? how about Dijkstra's guarded conditional? 2. recursive contracts how could we introduce recursion into the definition of contracts? 3. iteration can we define a while loop in terms of recursion? F. specification constructs what way could we specify contracts more abstractly to allow implementations (refinements) to make more decisions? can we allow for an unbounded number of choices? 1. relational assignments ------------------------------------------ RELATIONAL ASSIGNMENT def: Let R be a relation on states. Then {R} is an action such that, when started in a state s, our agent can choose a state s' such that s R s'. example: Let R2 be the relation such that s R2 s' iff val.y.s' == val.y.s mod 2 or val.y.s' == 50 So (y|->3) R2 (y|->1) and (y|->3) R2 (y->50) def: Let R be a relation on states. Then {R}^o, written [R] is an action such that, when started in a state s, the other agent can choose a state s' such that s R s' ------------------------------------------ when does our agent breach the contract {R} ? when can our agent satisfy the contract {R}; {q} ? when does the other agent breach the contract [R] ? when does our agent satisfy the contract [R]; {q} ? what refines the specification [y := n | n mod 2 == 0] ? what refines the specification {y := n | n mod 2 == 0} ? so who is a refinement better for? 2. pre-postcondition specifications G. correctness (1.7) ------------------------------------------ CORRECTNESS (1.7) def: Let p and q be predicates. S is correct with respect to p and q, written p {| S |} q, iff for all s that satisfy p, s {| S |} q holds ------------------------------------------ What ways can our agent win such a game? how does this compare to total correctness? 1. correctness problems ------------------------------------------ CORRECTNESS PROBLEMS The correctness problem: given p, S, and q, prove p {| S |} q The program derivation problem: given p and q, construct S so that p {| S |} q The program analysis problem: given S, find p and q such that p {| S |} q The backward program derivation problem: given q, find S and p such that p {| S |} q ------------------------------------------ H. refinement of programs (1.8) what is stepwise refinement? what is program transformation? How does it relate?