Optimizing Contract) Sample Clauses

Optimizing Contract). An optimizing contract C is a tuple C = (U, X, A, G, O), where • U is a set of uncontrolled (input) variables and X is a set of controlled (output) variables, with U ∩ X = 0/ and V = U ∪ X ; • A and G are sets of behaviors over V representing the assumptions and the guarantees, respectively, n a set of ports P, and a set of behaviors [[M]] over variables and • O : G → R is an n-dimensional objective function map- ports. Components can be connected to form larger systems by sharing certain ports under constraints on the values of certain variables. For simplicity, we use the term “variables” to denote both component variables and ports. An A/G contract C = (V, A, G) is a triple where V denotes the set of component variables, A denotes the assumptions, i.e., the set of behaviors that a component M expects from the | ∩ ⊆ environment, and G denotes the guarantees, i.e., the behaviors promised by M if the assumptions hold. A component M is a (valid) implementation of a contract C when A [[M]] G; we then say that M implements C and write M = C. A component ∪ | ⊆ ∪ E is a (valid) environment of C when [[E]] A; we then write E =E C. A contract C = (V, A, G) is in saturated form if G = G A where A is the complement of A. A contract C = (V, A, G) can be saturated by turning it into Cj = (V, Aj, Gj) where Aj = A and Gj = G A. C and Cj are equivalent, since they are characterized by the same sets of environments and implementations. In the remainder of the paper, unless otherwise specified, we assume that all contracts are saturated, as saturated forms will be used to define the main contract operations and relations.