Contract Entailment. Contract entailment is a relation ≤ such that, when c ≤ d holds, each value that satisfies c can be used where a value that satisfies d is expected. When c and d are flat contracts, ≤ boils down to the set-theoretic inclusion between the values that satisfy the respective predicates. For example, flat_c (≥ 3) ≤ flat_c (≥ 0) since every number greater than or equal to 3 is also greater than or equal to 0. To define entailment when c and d are session contracts, it helps to recall the analogy of contracts as specifications for the messages that can be sent on and received from a session endpoint. In this case, c ≤ d holds if two conditions are satisfied:
1. Every message that can be received from an endpoint satisfying c can also be received from an endpoint satisfying d.
2. Every message that can be sent on an endpoint satisfying d can also be sent on an endpoint satisfying c. Note that c and d occur in different orders according to the direction of exchanged messages. With these intuitions, we formalize entailment below: Definition 5 (contract entailment). We say that e1 entails e2, written e1 ≤ e2, if one of following conditions holds:
1. e1 ⇓ flat_c w1 and e2 ⇓ flat_c w2 and v ∈ w1 implies v ∈ w2;
Contract Entailment. Contract entailment is a relation ⩽ such that, when c ⩽ d holds, each value that satisfies c can be used where a value that satisfies d is expected. When c and d are flat contracts, ⩽ boils down to the set-theoretic inclusion between the values that satisfy the respective predicates. For example, since every number greater than or equal to 3 is also greater than or equal to 0. To define entailment when c and d are session contracts, it helps to recall the analogy of contracts as specifications for the messages that can be sent on and received from a session endpoint. In this case, c ⩽ d holds if two conditions are satisfied:
(1) Every message that can be received from an endpoint satisfying c can also be received from an endpoint satisfying d.
(2) Every message that can be sent on an endpoint satisfying d can also be sent on an endpoint satisfying c. Note that c and d occur in different orders according to the direction of exchanged messages. With these intuitions, we formalize entailment below: Definition 5.1 (contract entailment). We say that e1 entails e2, written e1 ⩽ e2, if one of following conditions holds:
(1) e1 ⇓ flat_c w1 and e2 ⇓ flat_c w2 and v ∈ w1 implies v ∈ w2;
(2) e1 ⇓ end_c and e2 ⇓ end_c;
(3) e1 ⇓ !c1;d1 and e2 ⇓ !c2;d2 and c2 ⩽ c1 and d1 ⩽ d2;
(4) e1 ⇓ ?c1;d1 and e2 ⇓ ?c2;d2 and c1 ⩽ c2 and d1 ⩽ d2;
(5) e1 ⇓ !flat_c v1.w1 and e2 ⇓ !flat_c v2.w2 and v ∈ v2 implies v ∈ v1 and w1v ⩽ w2v;
(6) e1 ⇓ ?flat_c v1.w1 and e2 ⇓ ?flat_c v2.w2 and v ∈ v1 implies v ∈ v2 and w1v ⩽ w2v;
(7) e1 ⇓ !c1.d1:e1 and e2 ⇓ !c2.d2:e2 and c2 ⩽ c1 and d1 ⩽ d2 and e1 ⩽ e2;
(8) e1 ⇓ ?c1.d1:e1 and e2 ⇓ ?c2.d2:e2 and c1 ⩽ c2 and d1 ⩽ d2 and e1 ⩽ e2. Condition 1 formalizes the set-theoretic inclusion relation between sets of values that satisfy given predicates, whereas condition 2 relates the contract end_c with itself. Conditions 3–4 deal with non-dependent contracts. Entailment is covariant on input prefixes, contravariant on output prefixes, and always covariant on continuation contracts. For example, we have !flat_c (≥ 0);end_c ⩽ !flat_c (≥ 3);end_c because the contract on the left-hand side imposes weaker requirements on the messages that can be sent on the endpoint. On the other hand we have ?flat_c (≥ 3);end_c ⩽ ?flat_c (≥ 0);end_c for the contract on the left-hand side provides stronger guarantees on the messages that can be received from the endpoint.
