Parametric Contracts Sample Clauses

Parametric Contracts. We model the contractual use of a software component at design- or reconfiguration- time as follows [5]: the requires interface represents the pre-condition of the component, as it describes the conditions the component expects its environment to fulfil in order to operate. The provides interface represents the post-condition of the component, as it describes the services the environment can expect the component to offer, if the pre- condition is met by the environment (This corresponds to ▇▇▇▇▇ design-by-contract principle [6], but is lifted from methods to components). However, if quality attributes are included in interface descriptions, this single pair of pre- and post-conditions is insufficient as it does not model the dependency of a component’s quality attributes (such as reliability or performance) on its context [4] 1. Therefore, we need to model the dependency between the context’s quality attributes and the component’s quality attributes depending on those. On the functional level we found service effect automata [7] useful. A service effect automaton is a finite state machine, describing for each service implemented by a component, the set of possible sequences of calls to services of the context. Therefore, a service effect automaton is a control-flow abstraction. Control-statements (if, while, etc.) are neglected, unless they concern calls to the component’s context. As an example, consider the following code (see figure 1, left hand side) and its associated service effect automaton (see figure 1, right hand side): 1 Although less obvious, even the mere functionality to be provided by a component depends on the context [7]. void DoOrderBilling(ListOfOrders orders, CCServer myCCServer) { myCCServer.Connect( resources.GetCCServerURL()); foreach (Order o in orders) { if (!o.HasValidCC()) { / Connect / BillCashOnDeliver BillCashOnDeliver(order); } else { myCCServer.Transfer(order); } / HasValidCC connected CCStatus known / Disconnect / Transfer myCCServer.Disconnect(); }