Design by Contract Using Meta-Assertions Isabel Nunes, University of Lisbon, Portugal

TOOLS USA 2002 PROCEEDINGS PDF Version

Abstract

Contract writing for methods in classes that are clients of other classes can bring undesirable effects, like the increasing in class coupling and encapsulation decreasing. We propose a pattern to the design of class contracts that helps producing contracts that preserve low class coupling and data encapsulation. The expressive power of existing assertion languages is insufficient, however, to write these contracts. In order to fill this lack we propose meta-assertions, and we define rules for a grammatically and semantically sound expansion of meta-assertions in order to be able to monitor contracts at run-time using already existing tools.

1 INTRODUCTION

The use of contracts to establish the rights and obligations of clients and suppliers is becoming widely accepted in the construction of reliable object-oriented software systems.

In what concerns the construction of classes, the design by contract programming discipline [Meyer97] stresses the need to precisely define the behaviour of modules through claims and responsibilities – the contracts. The specification of contracts – pre and post-conditions – for each method of a type is possible in several existing assertion languages – iContract [iContract], COLD-1 [Jonkers91], Jass [Bartezko01], Eiffel [Meyer97], ContractJava [Findler01], Larch family [Guttag85], JML [Leavens00] among them. Some of these – Jass, iContract, Eiffel – as well as others, allow the monitoring of contracts at runtime.

Specifying contracts is very important to the correct reuse of software. Clients must know the rules of the business. Thus, methods must make their pre and post-conditions public knowledge. Moreover, contract specifications are important insofar as they can be used to verify program properties [Havelund00, Jacobs01, Van der Berg01].

Testing contract assertions at run-time is also important because it is a way to ensure that methods are executed only if they are given the proper conditions, and to ensure that only correct implementations of specifications are executed.

The several languages of assertions, and monitoring code generation tools that exist allow the specification and, eventually, the runtime checking of very powerful and elegant contracts. This is definitely so for classes as simple as Stack, Point or Account. However, the task of specifying contracts for methods in classes that are clients of these simple classes, is harder and can bring undesirable effects like the increasing in class coupling and encapsulation decreasing. The benefits we gain from writing monitorable assertions that do not suffer from these defects can turn to be considered as not enough rewarding when compared with the effort we must put in that task.

We propose a general responsibility assignment pattern for design by contract that is to be used in the writing of assertions while avoiding the above mentioned undesirable effects. This way of doing design by contract demands for additional expressive power from assertion languages. We also propose a general extension for assertion languages while maintaining the semantics of simple assertions and reusing monitoring code generation tools that eventually exist for those languages.

The paper consists of five sections. In the next section we show, through the use of an example, how contracts should and should not be written if one aims at low class coupling and encapsulation of object components. The approaches that existing assertion languages allow to follow in the specification of this kind of assertions are not satisfying in what respects several criteria. Section 3 presents our approach – meta-assertions – in an informal way, stressing its benefits from several points of view. It also gives the formal syntax of meta-assertions and the rules that define its operational semantics. Section 4 presents the rules for the expansion of meta-assertions into simple assertions abstracting away the details of the assertion language that serves as the basis for meta-assertions. Section 5 presents the conclusions and further work.

2 MOTIVATION

Let us take a first example to show the reasons why we are compelled to write assertions in a given way, and the reasons why it is not the best way to write them. This example deals with points, polygons (whose vertices are points) and drawings (which are composed of polygons). Each one of these types defines an operation of movement by given distances both horizontally (dh) and vertically (dv).

The semantics of these operations are given, in a rigorous way, through axioms in the abstract data types (ADTs) that define types Point, Polygon and Drawing.

In order to build classes as correct implementations of the corresponding ADTs we have to implement each method of the classes in such a way that the axioms are true for each and every possible instance of the class. In what concerns the move operations, the relevant parts of these ADTs can be given by:

In order to create the types that implement these ADTs we shall define the assertions that specify their behaviour – the contracts for their methods – from the ADT's axioms and pre-conditions. We will use in this example a general assertion language that extends the syntax of Java expressions with several given constructs (forall – a quantifier, and old – to refer to values before execution, are the ones we use in this paper).

From ADT Specifications to Contracts

When we try to establish the correspondence between the ADT specifications and class assertions we should, among other things, create a post-condition for each axiom that involves a command auxiliary function (ones that return an object of the type being defined, as for example, move). When we think about implementing ADT command functions, [Meyer97], we usually abandon the ADT applicative kind of specification, in which all operations are modeled as mathematical functions (function move, for example, returns a new Point that results from moving the original one). Instead, we adopt the more imperative style that prevails in software construction (where structures are modified instead of producing new ones). By this reason, it is usual to implement command functions as procedures, that is, methods that do not return any value.

The axiom for the move operation in ADT Point suggests that the point coordinates change after a movement and it shows how they change. We would easily obtain the post-condition of the move method in type Point,

a)x()==old(x())+h && y()==old(y())+v

The object that results from moving the original point is the current object at the time the post-condition is evaluated (x() is implicitly applied to the current object); the x() coordinate of the original point object is given in a) by old(x()).

The meaning of the axioms for the move function in the ADT for Polygon can be expressed as the following post-condition for the move method in type Polygon,

The object that results from moving the original polygon is the current object at the time the post-condition is evaluated. So, vertex(i) is called over the moved polygon – the current object – and gives the moved vertex. As in the ADT's axiom, here we say that this moved vertex equals the vertex we would obtain if we moved the corresponding vertex of the original polygon (old(vertex(i)). The same reasoning could be applied to the move operation of type Drawing. These post-conditions assume that the result of the move methods in types Point and Polygon are functions that return a point and a polygon respectively (they are compared with the existing vertices and polygons). This goes against the above suggested idea that all methods that change the state are procedures, and which is itself consistent with the need for the clear distinction between commands, which change objects but do not directly return results, and queries, which provide information about objects but do not change them.

Moreover, any expression obj.meth(args) that appears in an assertion, represents the value that is returned by the call of method meth over object obj with arguments args. If we recall that one of the important roles of assertions is to allow the monitoring of executions, we should look at these obj.meth(args) expressions as real method calls.

The assertion in b) goes against the reasonable rule that one should not use operations with side effects in the specification of contracts that are to be monitored (in a monitored call, the invocation of move over old(poly(i)) would modify it. A classic example is the post-condition for the push operation on a Stack, pop().equals(old(this)) that is obtained from the axiom pop(push(X,S))=S. The evaluation of this post-condition at the end of the method execution would change the current stack by popping it the element just pushed, leaving it as it was before the push operation was executed.

Assertions should be written using queries only, that is, its evaluation should be without side effects. Taking this as a rule from here onwards, let us see then how these post-conditions could be written.

Contracts Can Bring Undesired Class Coupling

In order to say – in move method of type Polygon – that all vertices of a polygon have suffered movement we have to use the queries that type Point offers:

This post-condition completely defines the changes that were operated in the state of the system. It is also the only way we can write it because type Point does not supply any other way to show its changes after a movement. Nevertheless this post-condition is more revealing than it should.

In order to say – in move method of type Drawing – that all polygons of a drawing have moved, we have to limit ourselves to the queries that type Polygon offers:

This post-condition is also more revealing than it should. As a consequence, the clients of this type must know about type Point and understand some of its methods in order to understand the result of applying the move method to a drawing composed of polygons! Clients of type Drawing shouldn't have to know about the exact changes in the polygon's coordinates (a set of polygons abstracts away the structured set of points that constitute the drawing). The encapsulation that is shown in figure 1 should be maintained at the level of assertions too.

This post-condition increases coupling between the classes of the system. As we know, strong coupling brings undesirable designs due to the decreasing in extension and reuse. We should be able to act over a drawing of polygons solely through the polygons themselves. The ideal way to do this would be something like:

that would reveal the changes operated in the drawing only through their most direct state revealing queries.

These examples show how a well-known problem that software designers deal with frequently, can emerge when we try to design by contract. This problem, and proposed solutions, is described by design pattern "Don't talk to strangers" [Larman98], which is related to "Chain of responsibility" [Gamma95], to be used during OO system design.

The pattern places constraints on what objects should be sent messages to within a method. It states that, within a method, messages should only be sent to the following objects: i) the current object; ii) a parameter of the method; iii) an attribute of the current object; iv) an element of a collection which is an attribute of the current object; v) an object created within the method.

The intent is to avoid coupling a client to knowledge of indirect objects and the internal representations of direct objects. Direct objects are a client's familiars, indirect objects are strangers and a client should only talk to familiars, not to strangers.

Applying these ideas to the design of the Drawing's move method of our example would lead us to designing it as a call to the move method of each of its polygons (as was already suggested above in the ADT presentation). Likewise, Polygon's move method would be designed as a call to the move method of each of its vertices. This is shown in UML collaboration diagram in figure 2. This would be consistent with the design class diagram of figure 1, which presents the desired low coupling.

Our concern when designing by contract is the same, although in design by contract we deal with specifications that is, with assertions, not with prescriptions. So, the advice to follow here is "don't talk about strangers"! The familiars in this context are i) the current object, ii) the parameters of the method, and iii) all objects that are accessible through functions of the class. Furthermore we are constrained by the fact that assertions must have no side effects.

One possible approach would be to create several, and otherwise useless, methods that would reveal all about the class's internal objects and the internal objects of these ones or that would inform, in this case for example, whether a polygon had been moved for given distances. This has several drawbacks: i) the code in those methods – in the programming language in use – would be written manually, which brings an additional source of errors; ii) it may be the case that it is not possible to create any more methods in the supplier classes unless we extend it through inheritance. The additional effort that this approach requires can make design by contract unattractive.

Another approach could be to write contracts that refer to the contracts of other methods allowing to say, for example, that the result of moving a polygon is the same as the result of moving all its vertices. We see two possible ways to reach this goal.

One way to do this could be to create, for each method m in the supplier classes, two other methods that would evaluate the pre and the post-conditions of m. The post-condition in e), for example, would call the post-move method applied to all the polygons of the drawing. This has the same i) and ii) above described drawbacks plus: iii) in what concerns the methods written to evaluate post-conditions, the programmer would have to be able to compare the new state with the old state of an object, for a command that had not been executed (only its post-condition would be evaluated)... this is not a trivial thing.

The approach we advocate here allows to write assertions that talk about assertions of other methods without having to manually write any additional code. Furthermore, in order to be possible to monitor contracts at runtime, we propose a process of generation of (simple) assertions in some existing assertion language from these (meta) assertions, that can be automated. The assertions that will ultimately be monitored are assertions written in some existing assertion language. So, the automatic generation of code for monitoring, provided by existing tools, is fully reused. All the effort in designing by contract is put on the writing of assertions, not on coding.

3 META-ASSERTIONS – A PROPOSAL

The approach we advocate asks for an expressiveness that none of the assertion languages that we know possesses. Our proposal is a new construct, a kind of a meta-construct, for assertion languages that allows to refer to assertions of other methods.

This approach brings several enhancements to existing assertion languages and tools: i) it allows the writing of very simple and easily understandable assertions; ii) it helps keeping class coupling low; iii) it promotes encapsulation; iv) it eases the job of contract writers, of method implementors, and of client classes implementors. A discussion on the benefits that they bring to the several entities involved in software specification and implementation can be found in [Nunes02].

Informal Syntax and Semantics

The new constructs are »pre and »post, that are used to represent, respectively, the pre-condition and the post-condition of the method to which they are applied.

Let us return to the move operation for the Drawing type. With the proposed approach we would write this post-condition as:

which intended meaning is: after the execution of the command move applied to an object of type Drawing, the state is the same that results from applying the move operation to all its polygons. In other words, the post-conditions of all commands move applied to all the drawing polygons are true in the resulting state. These meta-assertions refer to assertions, not to methods. So, when they are monitored, there is no execution of methods move but, instead, the evaluation of the post-conditions of those methods.

In this way, we are able to represent the result of an operation by writing only the conditions that are of the direct responsibility of the enclosing class. We do this without creating unnecessary query methods for querying objects that are "strangers" to client classes.

When Monitoring Enters the Scene

How can meta assertions be monitored, that is, how can code be generated from them that can be executed before (pre-conditions) and after (post-conditions) the method code itself? Meta assertions by themselves cannot be evaluated by existing tools. They denote other assertions that, in turn, may denote other assertions. In order to evaluate a given meta assertion by an existing tool, we have to expand it until it is composed of simple assertions only. Informally, simple assertions are assertions that do not contain any of the »pre and »post meta constructs. For example, the (meta) post-condition of the Polygon's move method would expand to the (simple) post-condition:

Likewise, the (meta) post-condition of the Drawing's move method would expand to the (simple) post-condition:

Even if the assertions that are finally monitored are the ones that refer to second (and possibly lower) level information, the extra coupling that they bring do not imply the costs that are usually associated to high coupling. Let us see how.

When, in figure 3, the simple post-condition is generated from the meta post-condition of methA() in class A, an expression is obtained that refers to objects of types B and C: b().c().Pc. Usually, higher coupling brings more difficult extension, but this is not the case here: if the post-condition of methC() changes, the (meta) post-conditions of methB() and methA() do not need to change. Only the corresponding simple post-conditions must change; if the process of expanding meta assertions is automated, this is easily done automatically by recompiling types B and A in order for these simple post-conditions to be re-generated.

Thus, there is total encapsulation in what meta assertions are concerned, and almost total encapsulation in what the corresponding expanded assertions are concerned (depending on the re-compilation to generate the new simple assertions).

In order to check (meta) contracts at runtime, we depart from:

• i) a set of classes written in an existing OO programming language PL; ii) the (meta) contracts for those classes written in an assertion language MAL which is an existing assertion language AL (for PL) extended with meta-constructs;
  

and we want to:

• iii) generate the simple assertions in the assertion language AL as expansions of the original meta-assertions; iv) use the tools for monitoring code generation that already exist for the pair (PL,AL).
  

The idea is that all syntactic and semantic checking of simple assertions are done by the existing tool for AL. This can be so because we prove that meta-assertion expansion process preserves grammatical correctness and semantics.

Syntax of Meta-Assertions

As a first step we must specify the syntax of the meta-assertion language MAL as an extension of a base language AL. The syntactic notation we use is based on BNF. We list the various syntactic categories and give meta-variables that will be used to range over constructs of each category:

The assertions of MAL have the same structure as those of AL with the difference that the ones in MAL are the ones in AL augmented with elements of BMeta, that is, basic-metas. We assume that the structure of assertions – method calls, attribute calls, references to objects and expressions – is given elsewhere by the syntax of the assertion language AL that serves as the basis for MAL. This assertion language eventually depends on the programming language for which it is designed. We define the other categories in a way that is independent of the details of the chosen assertion language. The structure of the other constructs is:

The function applyP: Path x Memb is used to define paths in a way that is independent of the details of AL. If, for example, the assertion language in question were iContract or Eiffel, the result of applyP(p,memb) would be p.memb because that is the way how application of methods and attributes is done in those languages. If it were an assertion language based on Smalltalk the result would be p memb. We also consider that the category RObj of the assertion language has a special element denoting the current object (Current in Eiffel, this in Java, self in Smalltalk) and which we represent by cur(). We call target method the method corresponding to mc in a basic-meta.

In order to evaluate or to expand a given meta-assertion ma that is part of the contract for a method mth in a type ty, we need to be able to access information about some ty supplier classes: to evaluate basic-meta applyP(p,mc)»pre, for example, we need to access information about the members of p's type.

Consider the following sets of identifiers and corresponding meta-variables that will be used to range over their elements. These sets will constitute the context for the evaluation of meta-assertions and, later, for the process of expansion.

TYPEID – set of type identifiers ranged over by ty

ATTRID – TYPEID-indexed set of attribute identifiers ranged over by attr

METHID – TYPEID-indexed set of method identifiers ranged over by mth

PARAMID – METHID-indexed set of parameter identifiers ranged over by par

PRESTID – {pre, post} ranged over by prest

The following functions abstract away the details of the assertion and programming languages in which meta-assertions are based, allowing to represent information about types and assertions in terms of the sets of identifiers and of the syntactic constructs defined above. The way they are implemented obviously depends on the details of each assertion and programming languages.

The MembList function gives the method and attribute identifiers that are defined in a given type – its members. The Params function gives the formal parameters of a given method in a type. The functions TypeOf... give the identifier of the type to which the given method, attribute or object reference belongs. In the TypeOfRef function the third parameter – reference to object – can be a logical variable of the assertion language (for example in a forall construct) or it can be a formal parameter; that is why an extra argument is needed – the identifier of the method containing the assertion – in order to know the type of the reference.

The Meth and Attr functions give the method and attribute identifier, respectively, that correspond to a given method or attribute call.

The Cond function gives the meta-assertion that is the pre or post-condition – depending on its third argument – of a given method on a given type. We assume that the pre- and post-conditions supplied by this function are the ones for the given type and method. That is, it is not supposed oring pre-conditions with ancestor pre-conditions to obtain the pre-condition referred to by the meta-assertion, nor anding post-conditions with ancestor post-conditions to obtain the post-condition referred to by the meta-assertion. Its implementation obviously depends on the base assertion language. If this language supposes, like iContract and Eiffel, that, for example, the pre-condition written in a method is the result of oring it with its ancestors' pre-conditions, then function Cond has to be implemented in a way that returns this complete pre-condition. On the contrary, if the base assertion language supposes, like Jass and ContractJava, that the pre-condition written in a method is as it is (they generate code that check the hierarchical dependencies of assertions at runtime), then the Cond function has to result accordingly.

The BasicM function gives all the basic-metas that appear in a given meta-assertion. The Members function gives the method and attribute calls that appear in a meta-assertion that correspond to given method and attribute identifiers. Finally, the ActualPar function gives the expressions that constitute the actual parameters in the method call of a meta-path.

The following rules give us the type of a path. They establish a relation between elements of Path and TYPEID given a context composed of a pair of elements of TYPEID and METHID which represent the type or class and the method within which the path appears.

The type of a path is the type of the tail method/attribute of the path. The form ref for the path applies to the other possibilities.

Semantics of Meta-assertions

Next we present the semantics of MAL assuming a language AL as the base assertion language. We only present the rules for the operational semantics of basic-metas. We do not consider the evaluation of basic-metas which target method is not a command or procedure, that is, which target method is a function that returns a result, for obvious reasons. We consider that the basic-meta mc»prest is semantically equivalent to applyP(cur(),mc)»prest.

The semantics is given operationally through a set of rules (fig. 4) that, given a configuration that includes, among other elements, a meta-assertion and a state, gives a boolean value. The way rules are expressed is similar to the one adopted in [Winskel92].

Remember that the only command that is executed and that can change the state is the original one – the one that contains the original meta-assertion in its contract. Throughout the evaluation of the meta-assertions that compose the original meta-assertion, no more commands are executed – only queries are executed and these do not change the state.

So, the objects that are of interest, in what a (non-constructor) method is concerned, are i) the current object before the method has been executed and the same current object after the method has been executed; ii) the objects referred to by the actual parameters before and after method execution, insofar as they may be modified.

The objects that the method may create are of two kinds: i) local entities that are not interesting in what concerns the evaluation of the method contract; ii) other objects that happen to be components of the current object or of the objects referred to by the parameters. These latter objects are already included in the objects that we referred above as being the interesting ones.

The need for the old versions of the potentially modifiable objects has to do with the old construct that typically all assertion languages define. This construct changes the object to which is applied its operand path – in old p, p is applied to the object as it was before the execution of the original command method.

A state s is a pair <s(old),s(young)> where s(old), respectively s(young), represents the part of state s that contains information about the old, respectively young, versions of objects. These two elements of a state are mappings from objects to type-values pairs <dynamic_type,attribute_values>. We denote by s(v)[ref] the type-values pair corresponding to object ref in its v version. For example, s(old)[cur()] is the type-values pair that gives the dynamic type and the values of attributes of the current object in its old version.

We denote by Object(s,ref,p) the type-values pair <dynamic_type,attribute_values> that represents the object that results from applying path p to object ref in state s. We denote by s[valref] the state that is equal to s except in the value of ref which is equal to val.

If the original assertion is a pre-condition, the old part of the state is irrelevant, because pre-conditions are evaluated before method execution. If the assertion is a post-condition then both these parts are important and are eventually not equal.

A configuration is a tuple <ty,mth,ma,s,Lm> where ty> where ma is a meta-assertion belonging to method mth in type ty, and that is to be evaluated in state s₀. State s₀ is such that s₀(young) contains information about the current object cur() and about all the objects referred to by the method parameters as they are at the time meta-assertion ma is evaluated. The old part of s₀, s₀(old), contains information about the old versions (that is, as they were before the method was executed) of the objects that are referred to in old constructs of assertion ma.