Previous article

Next article


Design by contracts : analysis of hidden dependencies in component based applications

D. Enselme, G. Florin, and F. Legond-Aubry, Conservatoire National des Arts et Métiers, Paris, France

space TOOLS USA 2003
PROCEEDINGS


PDF Icon
PDF Version

Abstract

Components are increasingly used to create complex and distributed systems and applications. They are often viewed as simple servers, which limits their capacity for collective action. In this paper, we propose a method to simplify their assembly and their potential re-usability. We use the notion of dependency and contract between components to explicitly design an entity that guarantee the correctness of the built system. We introduce split contracts and delegations of properties to check, both at conception and execution time, the correctness of the built system. Our solution increases the independence of the participating entities by isolating the core components and transferring the aggregation into specific "glue" components.


1 INTRODUCTION

The Object Oriented approach was introduced to offer powerful tools and efficient structural design. Classes offer a clear hierarchical organization. However complexity remains in the interactions that tightly bind each object with the others. This hinders the development of large scale industrial applications. Components were introduced to enhance the isolation and the separation of concerns by increasing the granularity of the manipulated entities, and by giving them new capabilities. But if encapsulation gives abstraction power, it hides the specification of the component (and mainly its internal behavior). Components are black boxes without a "user manual".

Contracts were introduced in Objects by Helm [5]. This aimed to compensate the lack of methods to express relations between objects. They were used to specify behavioural compositions. Using contracts provides an orthogonal dimension to the one provided by the class structure. Techniques of development are more and more based on the component approach [3]. To improve these techniques and allow reuse, contracts were extended and adapted to them by Meyer [10] and Jezequel [6]. Usually, contracts are only associated to servers. That limitation is still present in contracts models. This is the significant anti-symmetry of the call because only servers imposes its conditions of use without even considering the clients nature.

This work1 offers developpers an integrated development environment with analysis tools that use more symmetric contracts to describe composition of components. This paper begins by stating current trends in the use of the contracts for components. Then we introduce a new point of view for the call of a component service. From this point, we set up contracts for this type of call and define a notion of compatibility between two contracts. From this basic definition, we then extend the compatibility notion to n components and define all the possible dependencies. Finally, we apply these notions to verify the integrity of an application developed with these contracts. To illustrate our approach, we present a simple cash dispenser example.

2 TOWARDS A COMPATIBILITY RELATIONSHIP

Components and contracts

A component is a cooperative composite entity similar to those described in Architecture Description Languages [8]. A component has multiple interfaces which are sets of operations - also called methods. Sometimes interfaces are grouped to make ports which become a point of interaction. A first attempt to introduce contracts in components was done in 1999 in the article "Making Component Contract Aware" [2]. It introduces four types of contract: syntactic, behavioral, synchronization, and quality of service. It specifies conditions and a unique contract carrying both client and server constraints.

An entity that interacts can only accept the contract (or one of its siblings) and respect it. This point of view limits the assembling capacity of a developer because some entities could have different compatible specifications without having any obvious relationship - i.e. same contract. Another restriction is that the contracts have to be used during execution in order to check the interaction validity. Finally, they are dedicated to an application and a specific platform even if adaptation remains possible. Contracts are made for a specific context therefore it is difficult to extract a component from the whole.

Tools like Jcontract [14], Icontract [18], Eiffel [9] implement "Design By Contract" assertions but for an Object Oriented Model not for components. Moreover they are used for test purposes and not at all for model checking.

To relieve these "dependence" and "checking" limitations, we choose to use "split" contracts. Each side has its own requirements and its own guarantees expressed as a set of properties. The client defines a set of required properties and the server a set of offered properties. If two entities have to interact, both split parties set a contract for the interaction. We are currently independent from a specific platform model like COM+, EJB [1], CCM [13], .NET [11]. All notions will be kept as abstract as possible. Though, In our model, stress is put on the semantic and the pragmatic viewpoints that is to say respectively on the functional and non-functional properties of a component. This document mainly deals with the description of interactions between components using contracts but wholly viewed as collaboration [15]. Contracts define dependencies in relations and interactions involving elements of the application. We associate, as in the CORBA CCM Model [16], to each interaction, specifications which accurately set the required service context (the client point of view) and the offered service context (the server point of view). Specifications are expressed by pre and post-conditions. Assertions determine the guarantees and the obligations applied to each participant in interaction. Server and client have to specify required conditions that the server and client must provide. If the server or client do not provide them, the binding won't be established.

Compatibility and sub-typing

Firstly, we introduce a compatibility notion between two components which leads us to define a compatibility relation between services (resp. interfaces, operations). Roughly speaking, this notion enables the substitution of one component (resp. service, interface, operation) by another one. A classical compatibility notion is given by the sub-typing notion : a type T is a subtype of a type T' (noted T <: T') if each value of T can be used in a consistent manner for each expected values of T'.

Our compatibility notion is based on an extension of sub-typing. To define the compatibility between two operations, we extend the classical sub-typing notion. We denote PO <: RO the compatibility of a Required Operation (RO) and a Provided Operation (PO). To check this newly defined compatibility, we add a specification to the involved operations. These specifications are composed of a set of properties. From now on, the properties describe the operations. We set SPO (resp. SRO) as the specifications of PO (resp. RO).

Services are too often under-specified but this is the only data (aside testing) that we can rely on and programmers always use the specifications for the important parts of the new designed component. So when we talk about compatibility between PO and RO, we mean compatibility between their respective specifications: SPO<: SRO.

Moreover, we can distinguish different levels, or so called point of view, in the specifications. Compatibility can be considered from many viewpoints. We use a classification deduced from the Natural Language Processing point of view. There is the syntactic level which deals with the signature and the manipulated data. The semantic level which deals with the functional properties of the service. And the pragmatic level that deals with the difficulties raised by the component environment and the way it is used. Usually the compatibility relationship uses sub-typing. We enforce that an operation o of type T is semantically compatible with an o' operation of T', if they have the same number of parameters and the same identifier, if the contra-variance of in parameters and the covariance of out parameters are confirmed. The contra-variance of in parameters asserts that they are in reverse order from the sub-typing relation. The covariance of the out parameters asserts that the parameters carry out the same sub-typing relation order.

The following two definitions illustrate the contra-variance of the in parameters for a provided and a required operation:

  • Provided Operation : void an_operation (in long parameter)
  • Required Operation : void an_operation (in int parameter)

The following two definitions illustrate the covariance of the out parameters for a provided and a required operation:

  • Provided Operation : void an_operation (out int return_param)
  • Required Operation : void an_operation (out long return_param)

This prohibits the sub-typing relationship for the inout parameters. This definition is one possibility among many others but it has the advantage of limiting the semantic variations of operations having the same signature (syntactically compatible) but with a totally different semantic. There is no automatic solution. Only the human brain can make the difference. As this compatibility relationship relies on sub-typing notions, the relation is transitive but not symmetric. So we have¬ (PO <: RO RO <: PO).

Then comes the semantic compatibility. In component interaction, the specification SRO of a Required Operation (RO) is a set of properties required to prove the correctness of the client. In a similar manner, a provided operation (PO) and its specification SPO guarantees the "usage" properties of all correct implementations of a server. Figure 1 illustrates this issue.

Figure 1: Interaction between a provided and a required service

A call correctness can be asserted by determining the "compatibility" conditions in which a client wishing to use a service RO could use a PO service instead. So, the call correctness is stated as conditions to satisfy for RO to be replaced by PO. We choose to use the pre and post conditions formalism. In a non-distributed monolithic programming context, assertions are expressed in classic first order logic. We don't need a specific expression of knowledge because the process has a global vision of itself and its state. However in distributed, concurrent programming, there is no global state, there are only some partial views of the systems. Making a nonoutdated global view is difficult and costly in many ways. It is therefore imperative to introduce a knowledge expression language (an epistemic language) to reify the state of knowledge of the entities. Another point is the fact that elements are concurrently addressed so a temporal expression language is also necessary. Therefore, in the concurrent distributed environment of the components, we set a pre-condition (O_pre) as a modal logic predicate that can be temporal and/or epistemic [17]. This
predicate is evaluated just before the execution of the operation and sets the conditions of the proper realization of the interaction (and subsequently the service). In most cases, the constraints do not specify one unique coherent state but a family of acceptable execution historic that will lead to an acceptable execution. In the same way, a post condition (O_post) defines a set of potential correct futures (after the correct achievement of the service).

A compatibility definition

The specification of an operation compels to use a temporal logic. We choose to use the Temporal Logic of Action [7]. In TLA, an execution is viewed as a sequence of steps, each producing a new state by changing the values of one or more variables. We apply the same analogy for components and we consider an execution to be the resulting sequence of a succession of states that will take the semantic meaning of the studied component interactions. At the very instant where the operation is enabled, the O predicate is true. The same holds for the O ^ O_pre. After the O execution, the operation following O (noted nextO or XO) is enabled. The predicate XO^O_post is true at this very moment and the post conditions are verified. This invocation specification presumes the atomicity of the operation from the client point of view. At this granularity level, we do not provide any information on the behavior of O during its execution. So basically the execution can be symbolized by O ^ pre O ^ O_post as in figure 2.

In this context, we must introduce time, causality and epistemic expression tools but this is not the purpose of the current paper. The previous basic statement can be extended to express the semantic and temporal compatibility of an interaction by using the five following equations:

Figure 2: Temporal Logic Representation of an operation execution

  1. RO ^ RO_pre XO ^ RO_post
  2. PO ^ PO_pre XO ^ PO_post
  3. RO = PO ^ XRO = XPO
  4. RO ^ RO_pre PO ^ PO_pre
  5. XPO ^ PO_post XRO ^ RO_post

The first condition (1) tells that there exists a specification SRO of a RO which enables the client to move from one coherent state to another. The second expression (2) states the existence of a provided operation specification (SPO) which enables the server to pass from one coherent state to another. The three last conditions seal the relation of compatibility between the client and the server. The third condition (3) guarantees that the provided operation PO can be used instead of the required operation RO. In other words, the component can make a direct invocation without the need of a connector or an adaptator to link the PO and the RO. The fourth condition (4) imposes the contra-variance between the provided and required preconditions. The fifth condition (5) imposes the covariance between the provided and required post-conditions. In other words, before an invocation, each pre-condition from the client must be verified by the caller and at the return, each post-condition from the server must be in agreement with the properties of the called.

The pragmatic compatibility is the most difficult to define. It consists in the behavioural and environmental compatibility verification. Pragmatic properties are often difficult to analyse. They could be expressed totally by logical expressions but also as state-transition diagram. In this case specifying compatibility is equivalent to testing if the diagram of the PO is less constrained than the diagram of the RO. Typically, this is the notion of symmetries found in Petri nets. This type of compatibility will be transitive but the symmetry will not be guaranteed as it was in the other levels. A more complex definition of the compatibility can be defined for interfaces, which will impose a causal order between calls. However the techniques are exactly the same than those used to compare the method behavior.

Semantic and pragmatic constraints can be expressed with first order predicate logic2, second order modal logic3 and with different languages [19]. Our study does not limit itself to one of them but all services are to be specified using the same logic language. It is not our purpose to develop our own language so we check some of among the abundance of existing ones. Our preference goes to one of the most widely used: OCL. In addition, temporal extensions and some software checkers are available for free [12]. Unfortunately, a knowledge expression extension is still missing in OCL. This add-on could be very useful to formulate and manage the ways and means of the information diffusion and knowledge of a specific data among components. A possibility to deal with theses properties is to use a runtime checker, to test if a component bind itself with an unauthorized entity or/and get access to forbidden data.

Interaction contracts

One of the essential principles in an interaction contract elaboration is the compatibility between the properties of each contributor. The compatibility between both involved operation is a sufficient and necessary condition for the existence of a contract (Figure 3) because of the transitivity of the relation.

So we must have SRO<: SPO. If this conditions is not verified then the interaction and subsequently the composition is not possible. An interaction contract has a specification issued from a negotiation process between a client and a server on the base of the required and offered specifications. So a simple interaction contract is a specification SCO which uniquely types an interaction. The contract specification SCO replaces, in the application using the caller and the called, their respective specifications (SPO and SRO). The existence of the SCO is ensured by the relation transitivity. So we have:

  • PO <: CO <: RO
  • RO_pre CO_pre PO_pre (contravariance)
  • RO ^ RO_post CO_post PO ^ PO_post (covariance)

Figure 3: Representation of interaction contracts

A first trivial illustrative sample

Firstly, let us say that more informations and a more complex sample can be found on the project page of ACCORD4. But, to illustrate this, let us take a naive getCash operation, which withdraws cash from a bank account. The client coordinator has a required interface RIBank link with the bank component obtained through a provided interface PIBank from a bank component. The specified method is getCash. The Required Operation of the client component is:

To be more precise, it would have been interesting to introduce the epistemic modalities where the client would only know if the operation is possible or not without knowing the balance. However, the previous code only limits the amount of money a client can take to a maximum of maximum1 and imposes that the balance of the account will stay positive after the operation.

The specification SPO of the provided operation (PO) would be:

This specification only enables getCash operation with an amount lower than maximum2. The post-condition throws an alert message if the amount on the account is below a trigger value. In this case, the contra-variance hypothesis on the pre-conditions RO_pre PO_pre) enforces the following condition for the operation to be successful:

The maximum amount required must be less than the maximum amount provided. The covariance hypothesis on the post-conditions PO_post RO_post) are naturally satisfied because

So from these conditions, we can make a SCO which is compatible with SRO and SPO:

In SCO, we must adopt in the pre-condition with an adapted maximum called maximumC which must be less than maximum2 and in the post-conditions those from the client which are compatible but which enforce some more conditions.

3 COMPONENTS ASSEMBLY AND CONTRACTUAL DEPENDENCIES

Why interactions contracts are not sufficient

Some specific cases appear in the construction of the specifications of SRO or SPO. On one hand the programmer can use a "Component Off The Shell" along with the provided specifications defined by the "COTS". Henceforth, the developer accepts the post-conditions PO_post and makes them his own RO_post for the new implemented component. In the same manner, he uses the pre-conditions PO_pre for the RO_pre and tries to satisfy them. Therefore, the newly created component accepts all the conditions imposed by the specifications of the component with which it interact. Verifying the peer to peer compatibility between both elements is then trivial. This case often rises in top-down development methodologies. On the other hand, when the programmer develops a new component, he can use the specifications of a required operation to build a new component with a provided operation that will totally satisfy the required properties. This is the case of bottom-up methodologies.

But this is insufficient. A composite is composed of a set of components according to an assembly graph. As a component can be a composite itself, the abstract model is fractal. If there is no dependence between the specifications then the assembly is reduced to a succession of interaction contracts definitions. More often, there are dependencies between the specifications so the validity of the aggregation must be verified.

Figure 4: Structure of a composite

The component specifications are fixed and are not mutable at execution time. The Provided Service has a visible (public) part and a hidden (private) part with its respective specifications noted SV PO and SH PO. The Required Service also has a visible and hidden part respectively noted SV RO and SH RO. (figure 4).

Dependencies taxonomy

This model exhibits four categories of possible dependencies between components specifications (noted from 1 to 4 on figure 4):

  1. Type 1 identifies the link between a visible provided interface of the composite and an interface provided by member components of the composite.
  2. Type 2 identifies the link between the required visible interface of a member of the composite and a visible interface of it.
  3. Type 3 identifies the external links between components. They are the previously defined links between a required operation and a provided one.
  4. Type 4 identifies intra-components links. These are reified to support the dependencies created by the implantation of a service that are used by another one.

Figure 5: Dependencies of provided public services

Figure 6: Dependencies of required public services

Dependencies of provided services (type 1 links)

Links of type 1 hold a more or less complex delegation of an external visible provided interface that is to say an invocation of a service on the external visible part of a component can be transferred to a sub-element of itself. The selected hypothesis is the pure delegation. In this case, the provided specification SV PO that is rendered visible is the same as the specification of a provided service (SH PO) of a composite member. Another working hypothesis would be a delegation by compatibility. Then a specification of a visible provided service is compatible with the provided service of a member of a composite (SH PO<: SV PO). Another last solution would be a delegation by adaptation so that the provided visible service is an adaptation of an internal provided one (figure 5).

Dependencies of required service (type 2 links)

As previously mentioned, one solution is the pure delegation of a specified required visible service of a member component as a required visible service of the composite. And in a similar way to the type 1 link, we can use the compatibility delegation (SH PO<: SV RO) and adaptation delegation.

Dependencies between components (type 3 links)

In the context of an assembly, a component needs a required service RO according to a SRO specification. It also provides a service PO in agreement with to the specification SPO. In the general case, a dependency relation called RPD (Required on Provided Dependency) express that SRO rely on SPO by the relation SRO = RPD(SPO). Examples of such dependencies can be exhibited in static or dynamic links or at a larger scale in aspect oriented programming. With the static link, the copying mechanism of the provided specification to define the required specification is one sample of dependency. With a dynamic link a component receives a reference to another one at runtime. So, it depends only on the component that will finally really be invoked. Aspect Oriented Programming (AOP) [4] introduces an aspect component that require the service of a base component which is, at first sight, undefined.

The specification and the services for this aspect oriented component is the one offered by the wrapped component. This would enable AOP advantages of the high granularity level of component. A last case is when quality of service is used because it also implies numerous dependencies. For instance, the response time for a service relies on the final server and its intermediates. Then time overhead, parameter modification and so on can be introduced (Figure 7).

Figure 7: Inter composites dependencies

Internal Dependencies (type 4 links)

A composite provides a service PO according to a specification SPO. It requires a service RO with its specification SRO. SRO relies on SPO by a dependency function called Provided on Required Dependency noted PRD so that SPO = PRD(SRO). We have the same example as those previously quoted (figure 8).

Figure 8: Internal Dependencies of a composite

Figure 9: Internal structure and dependencies of a composite

So finally we can structurally define a composite with the schema of the figure 9.

The dependency equations system

The observation of the structure (figure 9) leads to distinguish four set of services:

  • a set of private provided services SH PO that are hidden and provided by a member component and can only be internally accessed by the composite.
  • a set of private required services SH RO that are hidden and must be offered by a member component (or a set of them) to the currently studied composite.
  • a set of public provided services SV PO that are provided by the component to the world.
  • a set of public required services SV RO that are required by the component. This link is often employed for shared public components.

From this list, we can now define the full equations for a typical component of the system.

  • Internal-External component dependency enforces that a private provided service (SH PO) rely on public required services (SV RO) and private required services (SH RO) according to a function PRDH so that SH PO = PRDH (SV RO ^ SH RO).
  • Internal-External component dependency enforces that a public provided service (SV PO) rely on public required services (SV RO) and private required services (SH RO) according to a function PRDV so that SV PO = PRDV (SV RO ^ SH RO).
  • External-Internal component dependency enforces that a private required service (SH PO) rely on public provided services (SV PO) and private provided services (SH PO) according to a function RPDH so that SH RO = RPDH (SV PO ^ SH PO).
  • External-Internal component dependency enforces that a public required service (SV RO) rely on public provided services (SV PO) and private provided services (SH PO) according to a function RPDV so that SV RO = RPDV (SV PO ^ SH PO).

A fixed-point solution

Defining a contract for a component leads to determine a unique specification SH CO which will replace the private offered (SH PO) and required (SH RO) specifications for each assembly link. Such a contract exists only if the compatibilities constraints settle incompatible dependencies between offered and required services (see paragraph "Interaction contracts"): SH PO<: SH CO<: SH RO. In fact, if the SH CO exists it can replace all the private specifications (SH PO , SH RO ) inside the equations so we should have :

This expression of the assembly, if it exists, relies on the contract specification defined for the private services (SH CO) and the required and provided services (SV PO, SV RO).

"No solution" traps

Until now, we supposed a good system design which enables an internal contract replacing all the contracts of the links inside the composite. To achieve this, we use the peer-to-peer compatibilities and delegations. However, some errors could appear in the design so that the algorithm gives no solution. Continuing the analogy between our study and the mathematical fixed-point method, two types of incompatibilities can at least be identified. The first one is the non-convergence of the method and the other one is the detection of a direct incompatibility.

The verification of the assembly may not be completely specified. This is due to the system under-specification or to a cyclic delegation that cannot be resolved. This is shown in figure 10. In this context, the method could help the conceptor to isolate the defective components, contracts or interactions.

The direct incompatibility is relatively easy to isolate because it is between two elements. A simple example would be an interaction between two semantically different interfaces; one relying on a transaction and another one relying on an atomic operation. The only solution to the problem is the insertion of a connector to do "the glue job". But this direct incompatibility can interfere at different levels.

The first and most simple case concern a required service and a provided one. There are many solutions to reconcile two participants. Mediator, Aspect Oriented Programming, Connector are some of them. The second one can arise in the case of delegations that are not pure; that is to say when a service is delegated in compatibility. A delegation is a transfer of service from one component to the other. It can be viewed as a structural interaction or as a cooperation. Two objects cooperate to achieve a common aim. This type of interaction is often not reified by the system. If an incompatibility arise, a wrapper with some kind of code must be used to reconcile the delegate and the delegated.

Figure 10: Cyclic relationship

4 A MORE COMPLEX (YET SIMPLE) EXAMPLE

Context

We set an academic sample for our exposé. A composite Cash Dispenser manages the distribution of money. It encapsulates some internal composites according to the structure presented in figure 11.

Figure 11: Global view of the system

The sub-elements of the main composite are the Human-Computer Interface, the Credential Verifier, the Stock Manager, the Printer and a Coordinator. The main composite is in external relation with a bank component for money transactions. To illustrate our point of view, we will partly describe the assembly of all these entities. We will limit ourselves to the relationship between the Coordinator and the other components. To keep the whole thing short, only semantic logic predicates will be used. Pragmatic properties will be excluded. From now, we will apply a bottom-up approach. The essential steps are:

  1. Verify the provided and required specifications compatibility.
  2. Solve the fixed point equations to get the provided specifications and the contracts.

Coordinator-StockManager relationship

The role of the coordinator component is to control the system tasks. The only operation that will be studied is the method getCash from the Coordinator. The behaviour of this operation is described on figure 14.

For a cash withdrawal, the Coordinator begins by checking the available stock. Consequently, a Required on Provided Dependency exists between the components Coordinator and StockManager (figure 12).

Figure 12: Coordinator-StockManager relationship

Figure 13: Coordinator-CredentialVerifier relationship

It is characterized, on the Coordinator side, by the existence of a required interface called "RIStock". A basic specification expressed by pre and post-conditions is:

The requirer commits itself to satisfy typing and ceiling constraints from its pre-conditions. As said before, the requirer expects the provider to fulfill conditions in return. To demonstrate the dependency, the post-condition has been set in order for the required interface of the Coordinator ("RIStock ") to be the one offered by the StockManager component: PIStock. This is the reason of the"Stock.PIStock.check_stock.post" line. The StockManager on its own sets up a selfsufficient provided interface called PIStock. It is specified by the following properties:

Coordinator-CredentialVerifier relationship

The coordinator then proceeds to the credential check of the client. To do this, it uses the authenticate component method (see figure 13).

The Required on Provided Dependency is featured from the Coordinator side by a RIAuthenticate:

And from the CredentialVerifier point of view, the PIAuthenticate is:

The required interface does not bind any peculiar condition and accept those from the provided interface.

Bank-Coordinator relationship

The coordinator has a required interface RIBank link with the bank component obtained through a provided interface PIBank. The specified method is withdraw_account.

and,

Figure 14: Internal Coordinator dependencies

Internal dependencies from the coordinator component

The simplified version of the operation getCash on figure 14 gives us the main interface PIMain of the coordinator:

Solving the fixed point equations

It is trivial to establish the external compatibility between the provided and required specifications of the encapsulated components. The required properties of the Coordinator are mostly defined by importing the provided properties of the used services. Solving the equations is equivalent to substitute the specifications (also presented in this paper as split contracts) for the interaction contracts and a global logical reduction of them in the Coordinator component.

After the dependencies substitution, we get:

And after the logical reduction:

Finally, a specification of the Coordinator provided interface getCash has been found. The next step in the bottom-up approach is to proceed to the resolution of the "Human-Computer interface" component contracts.

5 CONCLUSION

In this paper, we present a new component assembly approach based on a fixed point equation resolution. This method can be applied to a top-down and bottom-up accurate existing components aggregation. One difficulty is the lack of specification for required and provided services of industrial components. The syntactic signature is often the only specification. User manuals are not really usable to make formal verifications. Moreover, even when these specifications exist, manual or automatic verification is still difficult. Split expression provided and required specifications, when assembled, insure correctness in component based applications.

It also enables to have a better isolation of each component, a new easier way to bind them and a possibility to perform structural verification of application. As a future work, we intend to design a method to locate assembly flaws hence to correct a bad assembly.


Footnotes

1 This work is sponsored by the French government research contract RNTL ACCORD. http://www.infres.enst.fr/projets/accord/

2 When the subject of the sentence is an individual object (like Socrates in "Socrates is mortal"), then we are using first order logic.

3 When the subject is another predicate (like being mortal in "Being mortal is tragic"), then we are using second order logic or higher order logic

4 http://www.infres.enst.fr/projets/accord/lot1/index.html

 

REFERENCES

[1] A.Thomas. "Enterprise javabeans technology". White paper, Sun Microsystems, Inc., 1999.

[2] Antoine Beugnard, Jean-Marc Jézéquel, Noël Plouzeau, and Damien Watkins. "Making components contract aware". In IEEE Software, pages 38-45, June 1999.

[3] D. F. D'Souza and A. C. Wills. Objects, Components and Frameworks with UML: The Catalysis Approach. Addison-Wesley, http://www.catalysis.org, 1998.

[4] G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, C. Lopes, J.-M. Loingtier, and J. Irwin. "Aspect-oriented programming". In LNCS 1241, November 1997.

[5] R. Helm, I. M. Holland, and D. Gangopadhyay. "Contracts: Specifying Behavioral Compositions in Object-Oriented Systems". In Proc. of the OOPSLA/ECOOP-90: Conference on Object-Oriented Programming: Systems, pages 169-180, Languages, and Applications / European Conference on Object-Oriented Programming, Ottawa, Canada , 1990.

[6] J.-M. Jézéquel, M. Train, and C. Mingins. Design Patterns and Contracts. Addison-Wesley, October 1999.

[7] Leslie Lamport. "The temporal logic of actions". ACM Transactions on Programming Languages and Systems (TOPLAS), 16(3):872-923, 1994.

[8] Nenad Medvidovic and Richard N. Taylor. "A classification and comparison framework for software architecture description languages". Software Engineering, 26(1):70-93, 2000.

[9] B. Meyer. Eiffel: The language. Prentice-Hall, 1991.

[10] B. Meyer. "Applying Design by Contract". Computer, October 1992.

[11] Microsoft. .NET. http://www.microsoft.com/net/default.asp, 2001.

[12] Klasse Objecten. OCL Checker. Web site, Klasse Objecten, 1999.

[13] Object Managment Group. "Corba components - joint revised submission". Technical report, Object Managment Group, March 1999.

[14] Parasoft. jContract. Web site, Parasoft, 1996.

[15] P. Champagnoux, L. Duchien, D. Enselme, G. Florin. "Typage pour des composants coopératifs". In NOTERE 2000 Proceedings, November 2000.

[16] R.Marvie. "Corba components: la proposition unifiée, du modèle au objet au modèle des composants". Technical report, LIFL, May 1999.

[17] R. Fagin,J. Y.Halpern, Y. Moses, M. Y. Vardi. Reasoning about Knowledge. MIT Press, 1995.

[18] R. Kramer. "iContract - The Java Design by Contract Tool". Web site, iContract, 1999.

[19] S. Shapiro. "Second order logic, foundations, and rules". Journal of Philosophy 87, pages 234-261, 1990.

 

About the authors

Fabrice Legond-Aubry is a PhD student at CNAM ("Conservatoire National des Arts et Métiers", Paris, France) since 2001. He is currently working with the University Paris VI LIP6 laboratory. He is involved in the development of the JAC core framework (Java Aspect Components). He also works on components adaptability and re-usability by using aspects and contracts. In 2000, he graduated from the EFREI ("Ecole Francaise d'Electronique et d'Informatique ") engineering school.

Daniel Enselme is Assistant Professor in Computer Science at CNAM. He received the PhD from the University of Paris VI in 1985. He has been working on Natural Language Processing and is now interested in Component Based Software and Aspect Oriented Programming.

Gérard Florin is currently a University Professor in computer science at CNAM. He received the "doctorat d'état" degree from the University of Paris VI in 1985. His research interests included Stochastic Petri Nets, Distributed Computing and now software components and Aspect Oriented Programming.


Cite this article as follows: D. Enselme, G. Florin, F. Legond-Aubry: "Design by contracts: Analysis of hidden dependencies in component based applications", in Journal of Object Technology, vol. 3, no. 4, April 2004, Special issue: TOOLS USA 2003, pp. 23-45. http://www.jot.fm/issues/issue_2004_04/article2


Previous article

Next article