Incremental evaluation of OCL constraints

1 Incremental Evaluation of OCL Constraints Jordi Cabot1 and Ernest Teniente2 1Estudis d'Informàtica i Multimèdia, Universitat Oberta de Catalunya [email protected] 2 Dept. Llenguatges i Sistemes Informàtics, Universitat Politècnica de Catalunya [email protected] Abstract: Integrity checking is aimed at determining whether an operation execution violates a given integrity constraint. To perform this computation efficiently, several incremental methods have been developed. The main goal of these methods is to consider as few of the entities in an information base as possible, which is generally achieved by reasoning from the structural events that define the effect of the operations. In this paper, we propose a new method for dealing with the incremental evaluation of the OCL integrity constraints specified in UML conceptual schemas. Since our method works at a conceptual level, its results are useful in efficiently evaluating constraints regardless of the technology platform in which the conceptual schema is to be implemented. 1. Introduction Integrity constraints (ICs) play a fundamental role in defining the conceptual schemas (CSs) of information systems (ISs) [7]. An IC defines a condition that must be satisfied in every state of an information base (IB). The state of an IB changes when the operations provided by the IS are executed. The effect of an operation on an IB may be specified by means of structural events [17]. A structural event is an elementary change in the population of an entity or relationship type, such as insert entity, delete entity, update attribute, insert relationship, etc. The IS must guarantee that the IB state resulting from the execution of an operation is consistent with the ICs defined in the CS. This is achieved by ensuring that the structural events that define the operation’s effect do not violate any ICs. This process, which is known as integrity checking, should be performed as efficiently as possible. Efficiency is usually achieved by means of incremental integrity checking, i.e. by exploiting the information that is available on the structural events to avoid having to completely recalculate the ICs. Hence, the main goal of these methods is to consider as few of the entities in the IB as possible during the computation of IC violations. For example, a ValidShipDate constraint in the CS in Fig. 1.1, which states that “all sales must be completely delivered no later than 30 days after the payment date,” may be violated by the execution of the AddSaleToShipment(s:Sale,sh:Shipment) operation, which creates a new relationship between sale s and shipment sh, since sh may be planned for a date beyond the last acceptable date for s. 2 Sale id : Natural paymentDate: Date Shipment id: Natural plannedShipDate: Date 1..* * D eliveredIn Fig. 1.1. A conceptual schema for sales and their shipments To verify that ValidShipDate is not violated after the execution of the previous operation it is sufficient to consider sale s and shipment sh of the new relationship, as incremental methods do, rather than carrying out a naive evaluation which must check the previous constraint for all sales and shipments. In this paper, we propose a new method for coping with the incremental evaluation of ICs at the conceptual level. We assume that CSs are specified in UML [11] and that ICs are defined as invariants written in OCL [10]. For each IC ic in the CS and for each structural event ev that may violate it, our method provides the most incremental expression that can be used instead of the original IC to check that the application of ev does not violate ic. By most incremental we mean the one that considers the smallest number of entities of the IB. Our method ensures the most incremental evaluation of the ICs regardless of their specific syntactic definition in the original CS. If our method were applied to the previous example, it would return an expression whose computation would only verify that the value of the attribute plannedShipDate of sh does not exceed the value of the attribute paymentDate of s by more than 30 days. Since our method works at the conceptual level, it is not technology-dependent. Therefore, the most incremental expressions obtained by our method can be used to efficiently verify the ICs regardless of the target technology platform chosen to implement the CS. Therefore, our results may be integrated into any code-generation method or any MDA-compliant tool to automatically generate an efficient evaluation. To the best of our knowledge, ours is the first incremental method for OCL constraints. Several proposals have been made for an efficient evaluation of OCL constraints, but with limited results. Moreover, our method is no less efficient than previous methods for the incremental computation of integrity constraints in deductive or relational databases. A comparison with related research is provided in this paper. The research described herein extends our previous research in [2], in which we proposed a method for computing the entities that might violate an integrity constraint; this method provides partial efficiency results in the evaluation of ICs. The main limitation of that research was that the results were totally dependent on the particular syntactic definition of the IC chosen by the designer, which involved, in the worst case, an almost complete recomputation of the IC after certain structural events. For instance, with the previous definition of ValidShipDate, after the AddSaleToShipment operation, [2] would verify that the planned date of all shipments of s is correct with regards to the payment date (instead of considering just sh and s, which is achieved using the method we propose here). The paper is organized as follows. In the subsequent section we present several basic concepts. Section 3 describes our method for incremental integrity checking. Section 4 introduces an optimization for dealing with sets of structural events. An example of the method’s application is shown in Section 5. Section 6 compares our approach to related research. Finally, Section 7 presents the conclusions and points out further work. 3 2. Basic concepts Our method assumes that CSs are specified in UML [11]. In UML, entity types and relationship types are represented as classes and associations respectively, while entities are called objects and relationships are referred to as links. Additionally, the method assumes that textual ICs are defined as invariants written in OCL [10]. Graphical constraints supported by UML, such as cardinality or disjointness constraints, can be transformed into a textual OCL representation, as shown in [5]; therefore, they can also be handled by our method. As an example, consider the CS in Fig. 2.1, which was designed to (partially) model a simple e-commerce application. The CS contains information on the sales and the products they contain. Sales can be delivered split up into several shipments and shipments can be reused to ship several sales. Finally, sales may be associated with registered customers who benefit from discounts depending on their category. The CS includes three textual ICs. The first IC (CorrectProduct) verifies that all products have a price greater than zero and a max discount of 60% (the maximum discount permitted by the company). The second one is the previous ValidShipDate IC, stating that sales must be completely shipped within 30 days after the payment date (and that therefore all shipments of that sale must be planned before that date). Finally, NotTooPendingSales holds if customers do not have pending sales for an amount greater than the maxPendingAmount value in their category. Note that an IC in OCL is defined in the context of a specific type1 or context type, and its body (the Boolean OCL expression that states the IC condition) must be satisfied by all instances of that type. For example, in ValidShipDate, Sale is the context type, the variable self refers to an entity of Sale and the date condition (the body) must hold for all possible values of self (i.e. all entities of Sale). Category Sale P urchases 1..* name : String maxPendingAmount:Money discount: Percentage id : Natural date: Date amount: Money paymentDate: Date context Product inv CorrectProduct: self.price>0 and self.maxDiscount<=60 context Sale inv ValidShipDate: self.shipment->forAll(s| s.plannedShipDate<=self.paymentDate+30) context Category inv NotTooPendingSales: self.customer->forAll(c| c.sale->select(paymentDate>now()).import->sum()<=self.maxPendingAmount) SaleLine quantity: Natural 0..1 Customer Id: Natural name : String nationality: String creditCard: Strin g B elongsTo * 1 Product id : Natural name: String price: Money maxDiscount:Percentage descri p tion: Strin g 1..* * Shipment id: Natural plannedShipDate: Date address: Address 1..* * D eliveredIn Fig. 2.1. Our running example As we mentioned above, ICs must be checked after structural events have been applied. In this paper, we consider the following kinds of structural event types: 1 In UML 2.0, the context type may be either an entity type or a relationship type since both types are represented in the UML metamodel as subclasses of the Classifier metaclass. 4 - InsertET(ET): inserts an entity in the entity type ET - UpdateAttribute(Attr,ET) updates the value of attribute Attr. - DeleteET(ET) deletes an entity of entity type ET. - SpecializeET(ET) specializes an entity of a supertype of ET to ET. - GeneralizeET(ET) generalizes an entity of a subtype of ET to ET. - InsertRT(RT) creates a new relationship in the relationship type RT. - DeleteRT(RT) deletes a relationship of relationship type RT. 3. Determining the incremental expressions of an OCL constraint In this section, we describe the method we propose for obtaining the most incremental expressions that should be used instead of the original IC, to ensure that the IC is not violated when a structural event is applied to the IB. We start by providing an overview of the method in Section 3.1. Then, in Sections 3.2 to 3.4, we define the three main operators used in our method to obtain these incremental expressions. An implementation of the method is described in [3]. 3.1 An overview of the method A direct evaluation of the original OCL definition of an IC, i.e. the one specified in the CS, may be highly inefficient. For example, a direct evaluation of the constraint ValidShipDate (as stated in Fig. 2.1) after an event InsertRT(DeliveredIn), which creates a new relationship d between sale s and shipment sh, would require taking into account all sales (because this is the context type) and, for each sale, all its shipments (because of the forAll operator), leading to a total cost proportional to PsxNsh, where Ps is the population of the Sale type and Nsh is the average number of shipments per sale. However, if we take the structural event into account we may conclude that the following expression: exp ≡ d.shipment.plannedShipDate<=d.sale.paymentDate+30 suffices to verify ValidShipDate (since the IB satisfies exp iff ValidShipDate also holds). Evaluating exp only requires that two entities be taken into account: the shipment participating in d (d.shipment) and its sale (d. sale). Clearly, evaluating this expression is much more efficient than directly evaluating the original IC. The main goal of our method is to translate an OCL constraint ic into the set of most incremental OCL expressions that allow an efficient evaluation of ic every time a structural event is applied over the IB. In general, there will be a different most incremental expression for each IC and each structural event that may violate it. By incremental we mean that the evaluation of the expression does not need to take all entities of the context type of ic and all their relationships into account, since it can reason forward directly from the entities that have been updated by the structural event. The most incremental expression is the one that considers the lowest number of entities of the IB. Obviously, the more entities required to evaluate an expression the less efficient is its computation. We use inc<ic,ev> to denote the most incremental 5 expression for a constraint ic after a structural event ev has been applied. In the previous example, exp is the most incremental expression for ValidShipDate after the event InsertRT(DeliveredIn) has been applied. The events that may violate an IC are called potentially violating structural events (PSEs) for that IC and may be determined by the method proposed in [1]. Applied to our example, this method would state that only InsertRT(DeliveredIn), UpdateAttibute(plannedShipDate, Shipment) and UpdateAttribute(paymentDate, Sale) can violate ValidShipDate. Note that other events such as DeleteET(Sale) or UpdateAttribute(address,Shipment) may never violate that IC. The most incremental expressions of an IC must only be defined by events in the set of PSEs of the IC. Determining the most incremental expressions depends on the given PSE and on the structure of the IC. Moreover, it generally requires changing the context type of the initial IC, since we cannot guarantee that the context chosen by the designer to specify the IC is the most appropriate one as far as efficiency is concerned. Intuitively, our method works as follows. First, it selects from all possible context types for the constraint (those types referenced in the body of the IC) the most appropriate one with respect to the structural event (i.e. the one that will produce the most efficient expression at the end of the process for that event). Second, it redefines the body of the IC in terms of this new context type ct’. Third, it computes the instances of ct’ that may have been affected by the event. Finally, the incremental expression is obtained by refining the body of the IC to be applied only over those relevant instances. This procedure is specified in the following algorithm. Algorithm: Obtaining the most incremental expressions Given an IC ic, which is defined in terms of a context type ct and an event ev (where ev is a PSE for ic), the following IncrementalExpression algorithm returns the inc<ic,ev> expression: IncrementalExpression( ic: Constraint, ev: Event) : Expression Type bestContext := BestContext(ic,ev) Constraint ic’:= Translate(ic,ev,bestContext); Expression rel := Relevant (ic’, ev) return (Merge(rel, ic’)) where 1. BestContext(ic:Constraint, ev:,Event) returns the type that must be used as a context of ic to generate an incremental expression for ic after event ev. 2. Translate(ic:Constraint, ev:Event, t:Type) returns an IC ic’, which is defined using t as a context type, such that ic’ is equivalent to ic regarding ev. 3. Relevant(ic:Constraint, ev:Event) returns an OCL expression whose evaluation returns the instances of ct (the context type of ic) affected by ev. 4. Merge(exp:Expression, ic:Constraint) creates the final inc<ic,ev> expression by applying b (the body of ic) to all entities reached in exp (the expression computing the relevant instances). If the evaluation of exp returns a single instance (i.e. all navigations included in exp have ‘1’ as a maximum multiplicity), this operator just replaces all occurrences of self in b with exp. Otherwise, the final expression is exp-> forAll(v|b) where all occurrences of self in b are replaced with v. 6 Let us again consider the event InsertRT(DeliveredIn) and the constraint ValidShipDate. As we have seen their incremental expression is exp, which is obtained using our method in the following way: 1. BestContext(ValidShipDate,InsertRT(DeliveredIn)) = DeliveredIn 2. Translate(ValidShipDate, InsertRT(DeliveredIn), DeliveredIn) = context DeliveredIn inv newIC: self.shipment.plannedShipDate<=self.sale.paymentDate+30 3. Relevant(newIC,InsertRT(DeliveredIn)) = d, the new relationship created by the InserRT event over DeliveredIn 4. Merge(d,newIC) (i.e. inc<ValidShipDate,InsertRT(DeliveredIn)>) = d.shipment.plannedShipDate <= d.sale.paymentDate+30 We show in Appendix A that the expression generated by the previous algorithm is always the most incremental one. In the rest of this section we formally define the BestContext, Translate and Relevant operators. To facilitate their definition, our method assumes a normalized representation of the ICs. The normalization reduces the number of different OCL operators appearing in their body (for instance, replacing the implies operator with a combination of the not and or operators or the exists operator with a combination of the select and size operators). This representation is automatically obtained from the initial IC and does not entail a loss of expressive power of the ICs we deal with. All three operators work with the ICs represented as an instance of the OCL metamodel [10]. According to this representation, they can handle the OCL expression by forming the body of the IC as a binary tree, in which each node represents an atomic subset of the OCL expression (an operation, an access to an attribute or an association, etc.) and the root is the most external operation of the OCL expression. As an example, in Fig. 3.1 the constraint ValidShipDate is represented by means of the OCL metamodel. Each node is marked with the set of PSEs produced by that node [1] (i.e. the events that are PSEs of the IC because of that particular node). 3.2 BestContext(ic:Constraint, ev:,Event) The best context to verify an IC ic after applying an event ev to the IB is automatically drawn from the node where ev is assigned in the tree representing IC. We use nodeev to denote this node (when different nodeev exist we repeat the process for each node). The BestContext operator always returns the same result regardless of the original syntactic definition of ic, since all possible syntactic definitions of ic must contain nodeev (because all of them may be violated by ev). To determine the context type, we must consider whether nodeev participates (i.e. is included) in an individual condition or in a collection condition. Intuitively, individual conditions must be verified for each individual entity (for instance, each individual product must satisfy the CorrectProduct IC). In contrast, collection conditions must be verified by the set of entities affected by the condition as a whole (for instance, in NotTooPendingSales, the sum of all sales of a customer must satisfy the maxPendingAmount condition). Individual and collection conditions are formalized in Definitions 3.2.1 and 3.2.2. 7 :IteratorExp ( forAll) :OperationCallExp ( <= ) :AssociationEndCallExp ( shipment ) :VariableExp ( self ) :AttributeCallExp (plannedShipDate ) :VariableExp ( sh ) UpdateAttribute(plannedShipDate, Shipment) InsertRT(DeliveredIn) :AttributeCallExp (paymentDate) :VariableExp ( self ) UpdateAttribute(paymentDate, Sale) :OperationCallExp ( + ) :IntegerLiteralExp (30 ) Fig. 3.1. The OCL metamodel of ValidShipDate and its set of PSEs Definition 3.2.1 A node n participates in a collection condition when n is used to compute an aggregate operator. Formally, when n verifies that {∃n’| n’∈ PathRoot(n) and n’.oclIsTypeOf(OperationCallExp) and n’.referredOperation ∈ {size, sum, count}}, where PathRoot(n) is defined as the ordered sequence of nodes encountered between n (the first node in the sequence) and the root of the tree (the last one). OclIsTypeOf and referredOperation are elements defined in the OCL metamodel. Definition 3.2.2. A node n participates in an individual condition if it does not participate in a collection condition. Clearly, since individual conditions must hold for each individual entity restricted by the constraint, the most incremental expression will be the one that only takes into account the single entity updated by the event. The original IC must then be redefined in terms of the type of entity to obtain this expression. Proposition 3.2.3 Let ev be an event over an entity e (resp. relationship r) of type E (resp. R). If nodeev is included in an individual condition, BestContext returns the same type E (resp. R) as the best context. In our example, the constraint ValidShipDate may be violated by three different structural events, all of them included in individual conditions: InsertRT(DeliveredIn), UpdateAttribute(plannedShipDate,Shipment) and UpdateAttribute(paymentDate,Sale), as shown in the tree in Fig. 3.1. Their best contexts are therefore DeliveredIn, Shipment and Sale respectively. The same idea cannot be applied to events included in collection conditions since those conditions must be satisfied by the collection as a whole and not by each single instance. Thus, to consider the modified entity or relationship is not enough to verify it because, after every modification, the whole collection must be recomputed again and the other entities in the collection must also be taken into account. For this reason, in selecting the best context it must be ensured that, after each modification, only the exact set of entities involved in the condition is checked. 8 For instance, an InsertRT(Purchases) event (i.e. the assignment of a sale s to a customer c) may violate the constraint NotTooPendingSales. In this case, the maxPendingAmount condition must be satisfied by the set of sales of each customer; thus, after assigning a sale to a customer c, it is enough to verify the set of sales of c. In this way, the Customer type is the origin of the collection condition. Note that Category is not the origin since it is not the union of sales of all customers in a category who must satisfy the condition. Therefore, if the event ev in the call to the BestContext operator is included in a collection condition, the type defined as the origin of the collection is the best context. This will be especially true when dealing with sets of events (see Section 4). Definition 3.2.4 Given a node n, PathVar(n) is defined as the ordered sequence of nodes encountered between n (the first node) and the node representing the self variable (the last node) of the subtree to which n belongs. More precisely, PathVar(n) is computed as follows: - The first node is n. - For each node included in PathVar we also include its child (or the left child if the node has two children), if any. - When a node n included in PathVar represents a variable other than self (i.e. variables used in select or forAll iterators), we add as a left child the node pointed to in n.referredVariable.loopExpr (i.e. the node representing the iterator; referredVariable and loopExpr are associations defined in the OCL metamodel). Definition 3.2.5 Given an integrity constraint ic, an event ev and the sequence PathVar(nodeev), nodeor, the node origin of a collection condition is - The left child of a node n ∈ PathVar(nodeev), representing a forAll iterator, when a select iterator is not encountered between the self variable and n. - Otherwise, the last node in PathVar(nodeev) (i.e. the node representing the self variable). If following the self variable there is a set of nodes representing navigations r1...rn where all ri have a maximum multiplicity of 1, then the final nodeor is the node at rn. Proposition 3.2.6 Let ev be an event included in a collection condition. The type of the entities at nodeor is then returned as the best context. In the NotTooPendingSales constraint, Customer is the origin of the condition since it is the type of the entities accessed in the node previous to the forAll iterator (the node navigating to customers from category). Therefore, Customer is the BestContext for all events included in the collection condition (updates of the paymentDate and amount attributes and inserts of Purchases relationships). The PSEs UpdateAttribute(maxPendingAmount) and InsertRT(BelongsTo) are included in individual conditions; thus, their best contexts are Category and BelongsTo respectively (as determined by Proposition 3.2.3). 3.3 Translate(ic:Constraint, ev:Event, t:Type) Given an IC ic that has a context type t and an event ev, the Translate operator returns an IC ic’ defined over a type t’, t’ ≠ t, which is semantically equivalent to ic with 9 respect to event ev. Having applied ev over the IB, ic’ and ic are semantically equivalent when ic’ is satisified iff ic is also satisfied in the new state of the IB. The Translate operator extends the method we presented in [4] since the context changes required in the work reported here present two particularities that can be used in order to provide a more optimized redefinition than the one in the previous reference. First, t’ is the type returned by the BestContext operator (this implies, for instance, that t’ is referenced in the body of ic). Second, ic and ic’ need only be equivalent with regards to the particular event ev. Therefore, ic’ need not worry about all the literals of ic that cannot be violated by ev. For instance, given that the body of ic follows the pattern L1 and L2 (as CorrectProduct in Fig. 2.1) and that ev can only induce a change in the truth value of L1, ic’ does not need to include the verification of L2. L2 was true before ev was executed (since all the states of the IB must be consistent) and, since ev does not affect it, L2 will still hold after its execution. When it does not hold it is because some other event, ev’, has been applied. The incremental expression for ev’ will take care of this possible violation. Translate is defined in two separate steps. First, the tree is pruned to remove the irrelevant conditions. Then the remaining tree is redefined over the context type t’ to obtain the final body of the translated constraint ic’. Definition 3.3.1 Let ev be an event attached to a node nodeev. A node nand representing an AND condition may be pruned if {nand ∈ PathRoot(nodeev) and ¬∃ n’| n’ ∈ PathRoot(nand) and n’.oclIsTypeOf(IteratorExp) and n’.name=”select”}. Nand nodes are replaced with the child node nchild ∈ PathRoot(nodeev). Consequently, the other child of nand (i.e. the other condition) is removed from the tree. Definition 3.3.2 Given a pruned tree tr that represents a constraint ic defined using a context type t, an event ev and the new context type t’, the redefined tree tr’ that represents an equivalent IC ic’ defined over t’ is obtained according to the following steps (see [4] for a more detailed explanation and examples): - Determining the node nodet’. Nodet is the node ∈ PathVar(nodeev) whose evaluation returns entities of type t’. If t’ is a relationship type, nodet’ is the node previous to the navigation through a role of t’. - Replacing all subtrees that match the sequence seq=PathVar(nodet’) with a single node representing the self variable. - Replacing all other nodes that represent self variables with the subtree corresponding to the expression self.r1…rn (or self.r1…rn->forAll(v|) when the maximum multiplicity of some ri is greater than 1), where r1..rn are the roles needed to navigate from t’ to t (the roles opposite to the ones used in the ic to navigate from t to t’). Formally, r1...rn = Inverse(PathVar(nodet)) with Inverse defined as {∀n ∈ PathVar(nodet) | n.oclIsTypeOf(AssociationEndCallExp)  OppositeRole(n) ∈ Inverse(PathVar(nodet))}. - Adding the subtree that corresponds to the expression self.r1…rn->notEmpty() implies X (where X is the tree resulting from the previous steps) to ensure that only those instances of t’ related to a given instance of t are verified (otherwise, they were not involved in the original IC). 16 17. Wieringa, R.: A survey of structured and object-oriented software specification methods and techniques. ACM Computing Surveys 30 (1998) 459-527 Appendix A. Correctness results of our method In general, there exist many incremental expressions that can be used to verify a constraint after the application of an event over the IB. To prove the correctness of our method, we must demonstrate that, given an IC ic and an structural event ev, the most incremental expression inc<ic,ev> generated by our method is always the incremental expression for ev with a lower cost. As a criterion to define the cost of an OCL expression, we use the number of objects accessed during its evaluation. For instance, the following expressions could be used to check ValidShipDate after an InsertRT(DeliveredIn) event creating a new relationship d relating a sale s with a shipment sh: exp ≡ d.shipment.plannedShipDate<=d.sale.paymentDate+30 exp2 ≡ s -> forAll(sh|sh.plannedShipDate<= s.paymentDate+30) exp3 ≡ sh -> forAll(s|s.paymentDate+30>=sh.plannedShipDate) Our method returns exp as the most incremental expression since it requires accessing only 2 entities of the IB, while exp2 involves all shipments of s and exp3 all sales of sh. Definition A.1 Let Bexp be the bag of entities accessed during the evaluation of an expression exp. Given an entity e of type t, e ∈ Bexp if one of the following conditions holds: - e is the entity referenced by a variable included in exp. - The subexpression t.allInstances() or super.allInstances() (where super is a supertype of t) is included in exp - For each subexpression expi.r included in exp (where r is the name of a role) and for each entity e2 ∈ Bexpi, if e ∈ e2.r then e ∈ Bexp Definition A.2 Given an expression exp, its cost is defined as cost(exp)=| Bexp|. Given this cost model, we must characterize the set sinc<ic,ev> of all possible incremental expressions for the IC ic after the event ev and show that the cost of the inc<ic,ev> expression generated by our method (inc<ic,ev> ∈ sinc<ic,ev>) is the lowest one among other expressions in sinc<ic,ev>. We derive the set sinc<ic,ev> from the initial IC. The first element of sinc<ic,ev> is the expression exp’ resulting from applying the body of the initial constraint ic over the instances of t (where t is the context type of ic) affected by ev. Formally: exp’ := Merge( Relevant(ic,ev),ic) 17 We create additional incremental expressions by repeating this process for all constraints ic’ equivalent to ic (ic’ and ic are equivalent when the IB satisfies ic’ iff satisfies ic). There are two general kinds of transformations over an IC ic resulting into an equivalent ic’. We can either transform the body of ic (by replacing some operators with equivalent ones) or redefine the constraint using a different type as a context. With the first kind of transformations ic’ and ic present the same cost since the number of entities of the resulting expressions remain unchanged (for instance, replacing a constraint body like X → Y with the equivalent body not X or Y, does not affect the number of entities accessed in the subexpressions X and Y). Therefore, when looking for alternative incremental expressions we are only interested in the transformations that redefine the initial constraint in terms of a new context type. Definition A.3 Let ic be an IC, ct the context type of ic and ev one of its PSEs. Then sinc<ic,ev> is given by: {∀t | t ∈ TypesReferenced(ic)  sinc<ic,ev> = sinc<ic,ev> ∪ { Merge(Relevant(Translate (ic,ev,t),ev),Translate (ic,ev,t)) } } where: TypesReferenced return all types referenced in the constraint body. An entity type E ∈ TypesReferenced(ic) iff an entity ∈ Bicbody is of type E. A relationship type R ∈ TypesReferenced(ic) if ic contains a navigation through one of the roles of R. Note that ct is always included TypesReferenced(ic). Note that each incremental expression is defined over a different context type. Therefore, we can reduce the proof of our method to the demonstration that the type returned by the BestContext operator is the one producing the most incremental expression (i.e. the incremental expression with a lower cost). Given an IC ic defined over a context t, we do not need to take types t’ ∉ TypesReferenced(ic) into account when determining the best context type. Note that, incremental expressions obtained using t’ must include a set a of navigations r1..rn from instances of t’ to instances of t in order to evaluate the body of ic. Such required navigation/s involves an extra cost that makes t (at least) a better option than t’. In the following sections, we prove the correctness of the two propositions defining the behaviour of the BestContext operator. A.1 Determining the best context for events included in individual conditions Proposition 3.2.3 Let ev be an event over an entity e (resp. relationship r) of a type E (resp. R). If nodeev is included in an individual condition, BestContext returns the same type E (R) as the best context. Proof We provide the proof for the UpdateAttribute(attr,E) event over an entity e included in an individual condition (proofs for the rest of the events can be obtained 18 applying a similar reasoning). This event is a PSE for the IC ic when ic includes a node n representing an access to the attribute attr. We prove that the incremental expression obtained using E as a context type is the one with the lowest cost by means of showing that 1 - using E as a context type the cost of evaluating the subtree having n as a root is the lowest one and 2 - the cost of evaluating the rest of the tree does not get worse. 1. In the incremental expression exp obtained using E as a context, the subtree representing the access to attr is compound by a node representing the variable e having n as a parent node. Therefore, the cost of evaluating this subtree is 1. When using an E’ (E’<>E), the subtree required to evaluate the node n must also include a sequence of nodes representing the required navigations from E’ to E before accessing attr, and thus, the cost will be >1. 2. Let be s a different subtree. Let be costs the cost of evaluating s in the initial ic (originally defined over a type t). In the worst case, when s is redefined in terms of E, the resulting subtree s’ includes a sequence of nodes seq=Inverse(PathVar(n)) representing the navigations from e to t (required to access the model elements referenced by the nodes in the original subtree s) and, as a consequence, the cost seems to be higher (cost(s’)=cost(seq)*costs)) Nevertheless, evaluating s in the incremental expression computed using t as a context (in principle the best option since then the cost of s is just costs) presents the same cost because we need to evaluate s over all affected t instances. This set of instances is precisely the set obtained using the previous sequence seq, and thus, the complexity is again cost(seq)*costs. A.2 Determining the best context for events included in collection conditions Proposition 3.2.6 Let ev be an event included in a collection condition. Then, the type of the entities at nodeor is returned as the best context. Proof We prove that the type Eor (the type at nodeor) is the best context by means of showing that the cost of expressions obtained using different types as context types does not improve the cost of the incremental expression obtained using Eor after applying a single event over the IB. Since, when dealing with set of events (see Section 4), using Eor provides additional benefits, this is enough to conclude that Eor is the best context. We provide the proof for the UpdateAttribute(attr,E) event over an instance e included in an collection condition (proofs for the rest of the events can be obtained applying a similar reasoning). This event is a PSE for the IC ic when ic includes a node n representing an access to the attribute attr. According to the definition of the node nodeor, precedes n in the tree (or nodeor=n), and thus, nodeor ∈ PathVar(n). We denote by diff the sequence of nodes between nodeor and n (diff= PathVar(n)-PathVar(nodeor)). In what follows we compute the cost of the incremental expressions obtained using as a context Eor, E and Ediff (where Ediff is the type of the entities at some node ndiff ∈ diff). A type Ei (where Ei is different from the previous types) cannot improve 19 the cost results since it would require a sequence of additional navigations to go from E to Ei and to reach Eor from Ei. We assume that ic consist solely of the collection condition col where the UpdateAttribute event is included in (as in the previous case, the cost of other possible collections, not affected by the event, do not change the best context election). We denote by costcol the cost of evaluating the collection condition for an instance of Eor. Let be expEor the incremental expression obtained using Eor as context type. cost(expEor) = cost(Inverse(diff))*costcol, where the first cost represents the number of entities of Eor affected by ev. For each affected instance, we verify the collection condition with a cost costcol. Let be expE the incremental expression obtained using E as a context type. cost(expE) = cost(Inverse(diff))*costcol, the same cost as before, since we are forced to navigate from the updated instance of E to the related instances of Eor to be able to verify the collection condition. Let be expEdiff the incremental expression obtained using Ediff as a context type. Cost(expdiff)=cost(Inverse(diff2+diff1))*costcol (where diff2 represents the subsequence of diff going from ndiff to n and diff1 the rest of nodes, i.e. the subsequence going from nodeor to ndiff). Note that in this case, after the UpdateAttribute event the affected Ediff instances are obtained using Inverse(diff2). For each affected instance we need to go back to the related Eor instances (using Inverse(diff1)) in order to evaluate the collection condition over them. From the previous results we can see that the cost of the incremental expression using Eor is not worse than the cost of the other expressions. Since, when dealing with set of events using Eor may provide a more efficient integrity checking, we may determine the incremental expression obtained using Eor as a context type, the most incremental expression. 20 Appendix B. Efficiency of the most incremental expressions The efficiency of the integrity checking process is highly improved when using the most incremental expressions obtained by our method instead of evaluating directly the original ICs. To illustrate these results, Tables B.1-B.3 compare the cost of using the original ICs (as defined in Fig. 2.1) with the cost of using the corresponding incremental expressions (as stated in Table 5.1), after each PSE. In the tables, we abbreviate the names of the entity types appearing in the CS (ca represents the Category entity type, cu represents Customer, s represents Sale, sh represents Shipment and p represents Product). Then, PEt stands for the population of the type ET (for instance, Ps represents the number of instances of Sale) and NEt1-Et2 stands for the (average) number of entities of Et2 related with an entity of Et1 (for instance, Ns-sh represents the average number of shipments per sale). Table B.1 Cost comparison for ValidShipDate Event Cost(MaxSalary) Cost (Incremental Expression) InsertRT(DeliveredIn) Ps x Ns-sh 2 UpdateAttribute(paymentDate) “ 1+1xNs-sh UpdateAttribute(plannedShipDate) “ 1+1xNsh-s Other events “ 0 Table B.2 Cost comparison for NotTooPendingSales Event Cost(MaxSalary) Cost (Incremental Expression) UpdateAttribute(maxPendingAmount) Pca x Nca-cu + Pca x Nca-cuxNcu-s 1+1xNca-cu+1xNca-cuxNcu-s InsertRT(BelongsTo) “ 1+1xNcu-s+1 InsertRT(Purchases) “ 1+1xNcu-s+1 UpdateAttribute(paymentDate) UpdateAttribute(amount) “ 1+1+1xNcu-s+1 Other events “ 0 Table B.3 Cost comparison for CorrectProduct Event Cost(MaxSalary) Cost (Incremental Expression) UpdateAttribute(Price) Pp 1 UpdateAttribute(maxDiscount) “ 1 InsertET(Product) “ 1 Other events “ 0