Contract Entailment Clause Samples
The Contract Entailment clause defines how the terms and obligations of a contract extend to related parties or subsequent agreements. In practice, this clause may specify that certain rights, duties, or restrictions outlined in the original contract automatically apply to successors, assigns, or affiliates of the contracting parties. By doing so, it ensures continuity and consistency in the enforcement of contractual obligations, preventing parties from circumventing responsibilities through transfers or restructuring.
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.
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;