"Design by contract"
JaWA
JaWA-Precompiler
translated by Holger Becker
The following document describes the use of the JaWA-precompiler including all of its options and configuration possibilities. After a thematic introduction the extentions to Java are explained. An introductory example illustrates both the use of the JaWA-precompiler and the method for a systematic software development by means of abstract data types in practice.
The following terms are meant to present a first survey. A more detailed description is given in the introduction.
"Design by contract"
JaWA
JaWA-Precompiler
... to have a look at the application of the JaWA Precompiler in an example ,
... to get in touch with the aims of the language JaWA,
... to know what an abstract data type
(ADT) is,
... to look at the extensions of JaWA
to Java,
... to compare the possible translationmodes
... to know how to use the precompiler,
... to download source codes or the documentation
In this chapter a thematic introduction into the problems in the development of correct software is given and it is discussed how JaWA tries to solve these problems. The chapter does not directly serve the purpose of describing the JaWA-precompiler; it rather explains the background that led to its development as part of a thesis. The language extensions, the use, and the configuration possibilities will be discussed in the following chapters.
The chapter is divided into the following sections:
Although the design and use of complex software systems has made it possible to accumulate much experience and a considerable technical know-how in the area of electronic data processing, it is still very difficult to develop error-free software. However, computers are used in areas in which errors can lead to disastrous consequences. The task of developing software has become even more difficult due to the complexity of computer systems that has increased enormously in recent years and that requires teamwork and project management. Additionally, the problems have not become easier in view of calls for reusability which is an essential aspect of object-oriented methods.
Software bugs can be very expensive. Still, for most languages there is no satisfactory concept for the development of reliable software. Formal languages for the systematic specification of all tasks a program has to perform can be useful tools. They often meet with considerable opposition in the industry, though. This is because they require extra effort because they create an increase in work load. This effort is only regarded as economically acceptable in areas that are crucial in terms of security. Without a formal description, however, the validity of certain desired properties of the software system cannot be proven. Therefore, even after extensive test runs one can never be sure that the software is actually free from bugs. Developing software thus often means looking for compromises and weighing costs against correctness.
This is where the concept of Design by contract comes in. It tries to do justice to both aspects and promote reusability at the same time. The concept was suggested by Bertrand Meyer and bundles a plethora of theoretical and practical insights. It combines the object-oriented approach, abstract data types and methods taken from software verification.
The idea is made up of four major aims:
Formal specification
Documentation
Debugging
Software-tolerance
The language Eiffel was designed to put this concept into practice. It is object-oriented, generic, supports multiple inheritance and has an exception handler. Basically, Eiffel is not much different from other current object-oriented languages: they are quite comparable in terms of essential language elements for the programming and also in terms of expressiveness. However, Eiffel has a methodological background that is different from that of other languages. It is this background that opens up new perspectives for the development of software of a higher quality.
Even though Eiffel has attracted a large number of followers and is used in numerous commercial products it was not as successful as other languages like C++. This is certainly due to the fact that C++ is very wide-spread and has a long history in the beginnings of which with C a standard language for the systems programming on various platforms came into existence.
Java was published in 1991 by Sun Microsystems. This language was meant to succeed C++ and to be used mainly on the internet. Its syntax being based on C++, it contains a number of changes and improvements. Java was booming. It spread very rapidly and quickly turned into one of the most important languages for practical software development, especially in the area of distributed systems. As it supports dynamic loading of classes, systems can be distributed, developed and used all over the internet.
As part of a thesis the concept of design by contract was examined and transferred to Java. For this purpose certain instructions have been included in the language that make it possible to express assertions in the programs. These instructions have the form of comments so that such an extended program will still be accepted by the Java-compiler. A precompiler translates these comments into statements in Java, which then check the assertions during runtime and trigger exceptions in the case of violations.
The result of this work is the extended language JaWA (Java with Assertions), including the precompiler to translate the extensions. The chosen approach in the transference to Java opts for a completely transparent handling for the developer. At the same time, it allows for numerous additional options for the precompiler by which the degree of the translation can be regulated.
In this work much importance was attached to an unproblematic and step by step transition phase, as an abrupt change in the methods is often rejected and does more harm than good. The developer shall appreciate the new methods and intensify their use gradually and thus ultimately be supported in the development of software that is much higher in quality.
Software development involves at least two groups of people. First, the developer or producer producing the software. Second, the user or customer who uses the software and who wants it to perform certain tasks. If the product is a library of software components, the programmer who uses this library for his own programs shall be regarded as a customer of these components.
The concept of Design by contract makes use of a metaphor, according to which there is a contract between both groups for the use of the software. The contract describes under what conditions the software may be used and which tasks it is supposed to perform. These conditions and tasks can be considered rights and obligations for both parties.
An obligation for one group is a right for the other and vice versa. The producer promises to render the services as described in the contract provided the user promises to meet the conditions. He therefore does not have to check these explicitly anymore which allows an easy and efficient implementation. The user gets a guarantee for these services provided he satisfies the conditions. The contract can thus be regarded as a specification of the software.
The idea is to check whether the contract is satisfied by a formal description of the conditions and the services. For this reason correctness formulae are included in the software components on the basis of an operational semantics. A correctness formula:
{p} S {q}
consists of a precondition p, a program S and a postcondition q. It basically means that a program is correct with respect to p and q if after the execution of S the condition q holds as long as S was started in a state which fulfilled p. Provided that p, the program guarantees that q is fulfilled. Unlike in the case of software verification, the correctness formulae are not statically verified but are dynamically checked during runtime.
In object-oriented languages each method call of an instance can be regarded as the execution of an independant program in such a way that the arrays of the respective class are global variables. The precondition in the correctness formula expresses the conditions under which the method call is allowed, and the postcondition contains those tasks that are supposed to be performed by the call.
The assertions in the correctness formulae used in this connection are boolean expressions which may contain variables and method calls. These assertions can be translated by the compiler as conditional statements and thus be checked during runtime. By using the methods even complex conditions can be expressed as assertions. Examples for assertions are given in 1.4 What are assertions?.
In section 1.1 Motivation the four major aims of design by contract have been mentioned. They will now be described in more detail. Their mutual influence plays an important role in this respect and constitutes a fifth, indirect aim.
Formal language for specification
The most important aspect is the possibility of formal specification. Assertions are a mechanism directly integrated into the language by means of which this can be reached.
"The advantages of exact specification and a systematic procedure in the software development can hardly be overemphasized. (...) Assertions are an urgently needed method to describe exactly what is expected of each party and what is guaranteed."
It is important that assertions are just a subset of quantification theory, the subset which every developer is automatically familiar with because of his programming skills. He does not have to be able to use quantifiers but can think in terms of his own familiar language. In other words, he can make use of boolean expressions which may contain those indentifiers for data structures and methods defined in his program.Documentation aid
The documentation of the software system is considered a contract between user and developer. It must contain all assertions of the class. Thus, all rights and obligations are publicly known. That they are understood by the users is ensured by using only those boolean expressions in the assertions that are also used in the other instructions of the language. This is important as the user may not be familiar with formal methods.
It would certainly be impractical if after every change in the assertions changes in the documentation had to be carried out manually. Many software engineers share the view that the documentation should not be separated from the program. In Eiffel both are contained in the same file and can be automatically extracted by a tool called "short". Java supports this concept as well, the tool here being called "JavaDoc".
This automatic extraction has two striking advantages: there is no arduous copying (which would be necessary to include all assertions in the documentation) and there is no specification that always has to be up to date. This guaranteed consistency is an essential part of design by contract and will be described in more detail in chapter five.
Debugging aid
So far it was only possible to write the assertions into the program and thereby into the documentation as well. If one wants to guarantee that they are satisfied all assertions have to be checked during runtime. Only then can one be sure that the system is in a defined state. This task is supported by the computer. It generates the code which checks an assertion in consideration of inheritance. The extent of the assertions to be checked can be controlled by the modes given in 6. The checkmodes.
The choice of an appropriate mode is a question of the importance of efficiency and security. If efficiency is more important, the check is turned off by choosing the option NOTHING for the respective classes. This is advantageous in terms of time and memory since the compiler does not generate a code for the checks and no checks are consequently made during runtime. If security is more important, all assertions should remain active by choosing ALL. The amount of time can be estimated by the set of assertions used, if these are considered an expression in a conditional statement. At this point it is important to check assertions of the class invariant (including inherited assertions) at the beginning and at the end of a method. If method calls or complex expressions are used in the assertions, the time needed must be added as well.
The option PRECONDITIONS can be considered a compromise. The developer of the class assumes that the latter is free from errors. For this purpose he has tested it extensively. What happens if a customer uses the class carelessly? The assertions being in the precondition, there is no necessity for the developer to test the conditions once again. Therefore, unforeseen exceptions like division by zero may occur and possibly destroy the integrity of the system. The mode PRECONDITIONS is the default mode. It takes an additional time of about 20%.
Support of fault-tolerant behaviour
Up to now, by using assertions one can only describe what a program is supposed to do and then check these statements during runtime.
For such cases Eiffel is equipped with an exception handler. At the end of a method body a rescue-block can be stated which is called if the body triggers an exception. The purpose of this statement is to leave behind the system in a stable state (which is expressed as a class invariant). What is special about this kind of error management is that each method call is either successful or fails and that this is reported to the caller in either case. 1.6 Violations of the contract: success or failure discusses this point in more detail.
If no other precautions are taken, the error still leads to the termination of the system, but disasters are avioded as the error cannot spread any further. The class invariant will be described in 2.2 The class invariant: 'invariant' , the rescue-statement in 2.5 The rescue-block: 'rescue'.
Another possibility in connection with exceptions is offered by the retry-statement. It is stated within the rescue-block or in a method called from within the rescue-block. By means of the retry-statement another execution of the method body can be triggered which may possibly be able to satisfy the contract. The caller gets no information about this (except for the fact that the call has taken slightly more time than usual). A detailed description of the retry-statement will be given in 2.6 The retry-statement: 'retry'.
With these language elements the robustness of the system can be increased considerably. The result is a system that reacts in a controlled way even in exceptional situations and thus protects tha data in an optimal way.
Synergies
In the previous section the advantages of design by contract have been discussed at length. They are a powerful tool in the development of large software systems. However, as soon as one asks an experienced developer one frequently receives an answer along the following lines: 'In the course of my work I have developed a style of my own that already contains these concepts. So why should I switch over and learn a new method if I can't benefit from it?' Such an answer is by all means understandable. By disciplined work software can be produced that satisfies high demands of quality. For in one's specification one does try and formulate all conditions that have to be fulfilled when calling a method. And one naturally tries to avoid all situations that might lead to errors or even crashes. But experience with software systems has shown that in most cases this approach does not work. Even if the consequences are seldom as disastrous as in the Ariane-example, we have to ask why this is the case, why bugs creep into our programs time and again.
The answer is: consistency. Today's programs are of such an enormous complexity that one can rarely survey them or keep track of every single detail. Team work increases these problems. It is possible that the software contains sections one may never come across. One has to rely on the statements given in the documentation about the interfaces without being assured that these are actually followed.
Unfortunately, we are often left in the dark about some properties of the software. The famous 'undocumented functions' are a case in point. It is a pity that these functions cannot be used if this allows more elegant or more efficient implementation. The phrase 'It's not a bug, it's a feature' is well-known.
However, what has not been discovered are the synergies. If by combining components we get more than the sum of the parts the term 'synergy' is used. The four advantages mentioned so far all have synergies. Every formally specified property is automatically documented and checked and can be handled by the program itself. The contract and the error management as well are always up to date. If one tried to reach the aims by four different methods, errors were bound to creep in as a result of inconsistencies. Thus, software of a higher quality can be produced with the same effort, or, to put it another way, the same quality can be achieved with less effort.
Assertions are statements about the state of objects. They describe properties of these objects, which have to be true at specific points of time during the execution of the program, and are either true or false.
In the extended language JaWA it is possible to insert assertions into the program in addition to the Java-statements. For instance, at the beginning of a method call the parameter 'a' of type integer might be required to be unequal to 0. This property is an assertion and in JaWA it can be included in the source code of the method by a require-statement:
/** require a!=0 **/
If in the class a method 'IsEven' is formulated that is assigned an integer-value and that returns a boolean value, a second condition might be that the value of the parameter 'a' be even:
/** require a!=0; IsEven(a) **/
In this connection nested method calls such as 'f(g(h(s)))' and accesses via references like 'a.f(x)' are allowed. Every boolean expression that can be formulated within a program can also be used as an assertion.
If at the beginning of a method call of an instance a precondition and a postcondition are formulated, the result is a correctness formula as described in 1.2 Design by contract. On the basis of an operational semantics statements about the correctness of the software can therefore be made. However, the JaWA-precompiler will not make any verifications. It will rather translate the assertions into Java-statements which check (during runtime) if the respective condition is met.
Assertions do not occur on their own, they are always part of one of the following statements:
In Java there is a new kind of comment, the so-called documentation comment. The Java tool JavaDoc automatically extracts these from the source code. All assertions which are part of the contract are therefore stated as documentation comments. This refers to preconditions and postconditions for methods and the class invariant. The remaining assertions in loops or the check-statement are stated as ordinary comments. They serve the function that their own implementation may be understood and are not an inherent part of the contract.
Abstract data types (ADTs)
ADTs are appropriate tools for modelling independent software modules. They completely abstract from any possible realization (in particular from the language) and merely describe the behaviour of one component. They make it possible to define exactly all characteristic properties of a module without overspecifying it by oversublety in the implementation.
One important aspect of design by contract is the way the development of software modules is supported. For this purpose a description is used that is divided into four sections. These shall be illustrated by an example. This example describes the ADT stack, which is a stack over arbitrary elements. In chapter 2 the language extensions will be illustrated by methods of this class as well.
The four sections of the ADT stack shall now be discussed in more detail.ADT Stack[X]
TYPES
Stack[X] , X , BooleanFUNCTIONS
new : --> Stack[X] empty : Stack[X] --> Boolean push : X x Stack[X] --> Stack[X] pop : Stack[X] --> Stack[X] top : Stack[X] --> XPRECONDITIONS
For all s: Stack[X]: pop : pre pop(s) = not empty(s) top : pre top(s) = not empty(s)AXIOMS
For all x: X and s: Stack[X]: empty(new()) not empty(push(x,s)) top(push(x,s)) = x pop(push(x,s)) = s
The section TYPES
This section contains the name of the ADT. This name also denotes the set on which the ADT operates by virtue of the functions defined in the following section. This set is called the codomain of the ADT. Further ADTs may be stated if they are needed for the definition.
If the structure of the codomain is not supposed to be or cannot be specified in any more detail, only a name is given. In this respect, genericity is supported as well. It demonstrates that an ADT depends on another one and can only be meaningfully described and used in connection with it. For instance, in the above example the ADT Stack is specified as depending on another ADT X. Any ADT may be used provided it fulfils the definition given for X. As there are no statements in this case, every ADT is possible. Thus, Stack[Integer] yields a stack for integers, Stack[Real] yields a stack for real numbers and Stack[Quittungen] yields one for receipts, whatever values these may ultimately have.
The section FUNCTIONS
Every function has a domain and a codomain. The so-called argument indicates that element of the domain for which the corresponding element of the codomain is supposed to be yielded. In combination with the section 'TYPES' they make up the signature of the ADT. In connection with software modules this has been called the syntax of the ADT.
It is important that we are here dealing with a function in the mathematical sense and not the execution of a program. A program runs and computes a result, whereas a function such as the sine function simply computes a result. It describes the connection between two values within the codomain of its type. It does not say how the result is computed, i.e. there are no side effects as can be the case with procedures.
This effect is desired. Bearing this aim in mind, by virtue of a function it becomes possible to assign a routine that has certain side effects an unambiguous task, without anticipating its realization. In the following two sections 'PRECONDITIONS' and 'AXIOMS' it will be shown how the semantics of the function can be determined. Before that, this idea shall be dealt with in a little more detail.
In the definition of the function push Stack appears twice. On the left, that stack is denoted on which the element is supposed to be put; on the right, that one is denoted that has come into existence after applying the function. Mathematically speaking, these are two different stacks that have merely been related to each other by a function.
If this ADT is to be realized as a software module, each routine in the implementation will be assigned a function in order to decribe in what way the respective stack has been changed by the call. In this perspective there is just one stack that is changed by services or operations in the form of procedures. The changes that are allowed are defined by the the associated functions uniquely and provably.
If the program has been defined completely by ADTs each program execution can be regarded as one large nested function call where the state in which the program was started has been related to the final state.
There are three kinds of functions or services:
Constructor functions
Access functions
Transformation functions
The section PRECONDITIONS
Each of the functions can be defined completely or partially. Completely defined functions can always be called and always yield a result.
With partially defined functions this is not always the case. They are not defined for certain arguments and they yield either no or an arbitrary result for these. For these arguments the function must not be called. In this section the domain of the function can be restricted. Thus, in the above example the only requirements for the domains of the functions pop and top are that they be used only for those stacks for which empty does not hold.
The section AXIOMS
This section presents the most important part of the ADT. In connection with the preconditions it defines the semantics of the functions and thus the tasks of the routines of the later implementation. It is therefore the basis for the checks. Each property of the ADT is formulated as a logical statement, for instance in terms of quantification theory.
In the example four statements are given. They first describes the property that each newly generated stack is empty at the beginning. The second statement adds that each stack on which a value has been put by push cannot be empty anymore. The last two statements describe the last-in-first-out property that characterizes a stack. If an element x has been put onto a stack and if top is called right afterwards, top returns exactly the element x. The element x is therefore on the top of the stack. If the function pop is called directly, the stack will be in exactly the state in which it was before.
This description gives a complete description of the ADT. Each object by which the above functions with the specified properties can be described is a stack. There may be any number of further properties. They do not play any role in this respect.
Note that it has in no way been prescribed how the functions can be realized. Not even the realization of the ADT in its entirety has been mentioned. It is left undecided if the implementation idea is used by an array or a concatenated list, for example, and if this idea is optimized by hash functions or double concatenations.
If the ADT is implemented later on by different classes, a mapping between these classes can be stated by means of which each statement over one class in transferred into the other class. Using the terminology introduced in the previous section, these classes are different signatures of the abstract data type stack and the mapping is the isomorphism between them.
In the previous section we have been discussing the topic of checking only. But what happens if an assertion is violated? The answer is: an exception is triggered.
Such an exception can then be caught and usually be handled accordingly. In JaWA there is a particular exception handler that is very different from that of other languages like C++, Java, or Ada. In these languages an exception can be used like a 'goto'-statement in order to exit a method at any position and then return to the caller. The possibilities are potentially dangerous as they may prevent errors from being caught.
Imagine a class 'Limited Stack' which represents a stack of limited capacity and which is implemented as an array. Let it have a method 'push' of which the implementation be based on another method 'setArrayField'. If the array is full and an internal counter exits the array, 'setArrayField' triggers an exception that is caught by 'push'.
The developer of 'Limited Stack' wants a robust module that is easy to handle. Thus, it is plausible if he ends the call of 'push' after catching the exception and if he includes in the specification the statement that 'push' may not be called if the stack is full.
For the user a dangerous error source is created here. It is possible that elements get lost completely during runtime if the check has been carried out sloppily. In practice this happens quite frequently because the check is not compulsory. This problem becomes especially important in the case of team work. If the class is already in use, an error is possibly let in through the back door by the changed specification that does not trigger any actions.
Such a behaviour is not what design by contract is about. There should be exactly two ways for a method to terminate:
Success:
Failure:
JaWA has two further language constructs to ensure that not every error leads to the termination of the whole system and to guarantee the integrity of the class that has been alluded to above. These are the rescue-block and the retry-statement.
The rescue-block can be stated at the end of the method body. If an exception occurs during the execution of the method, the body is terminated abruptly and the rescue-block is started. Here the developer can insert statements such that the integrity of the class is ensured. For instance, in a data base with a transaction concept the consistency of the data base is guaranteed by undoing those steps of the operation that have already been carried out. The exception is not deleted, however, but it reports the failure.
The retry-statement ensures further flexibility. It can retrigger the execution of the method body from within the rescue-block. If then all the conditions required for the success are satisfied, it has been able to fulfil the contract all the same. These retries remain invisible, if one disregards the slightly longer runtime.
Thus, the method call fails if and only if the method is left by ending the rescue-block. Furthermore, there is success if and only if the method is left by ending its body, possibly after a retry.
Rescue and retry are two exception handlers that handle the errors where they occur: in the method itself. They cannot spread and cause damage at other places; errors of the kind described above are avoided, as the changed specification is automatically integrated in the check during runtime.
In this chapter the assertions that are possible in JaWA will be described. The description of the syntax will be done in the form of grammatical rules and will be illustrated by means of a brief example from the class 'stack' for stacks of any elements.
The grammatical rules are stated in EBNF, terminal symbols are represented in'Courier', nonterminal symbols in 'Times'. Alternatives are separated by '|' and have been given a line of their own whenever possible. Optional information is given in brackets '[ ]'. To simplify matters, the rules for assertions have been written as documentation comments in '/**' and '**/'. '/*' and '*/' can be used in their place, though. However, only documentation comments from the tool 'JavaDoc' will be extracted.
The chapter is subdivided into the following parts:
As in Eiffel, for each method of a class in Java a precondition and a postcondition can be stated by the JaWA extensions. The precondition is at the beginning of the method body (directly after the opening brace), the postcondition is at the end (before the close brace). both are stated in the form of documentation comments.
The precondition consists of the key word 'require' and one or more assertions separated by semi-colons. As has already been mentioned in 1.4 What are assertions?, the assertions are boolean expressions as one might also use them in the method body. Thus, all attributes of the class (both arrays and methods) and the current parameters for the generation of complex expressions may be used.
Any number of assertions (separated by semi-colons) may be stated. The semi-colon connects the assertions like a logical 'and' so that the whole precondition ultimately is nothing but one boolean expression. The semi-colon can therefore be used in order to divide the expression into smaller and clearer parts and, if desired, to give each part a label of its own. The label precedes the expression and is separated from it by a colon.
Postconditions are constructed in the same way as preconditions, the only difference being that they must begin with the key word 'ensure'. They offer three further possibilities, though: First, each field of the class may be preceded by 'old_'. It represents the value of the variable before the method call. For instance, by means of an assertion like 'i = old i' it can be required that the value of 'i' be not changed by the call.
The second extension is the reserved word 'nochange'. It is a boolean expression that is true if and only if by the method call no array in the class has been changed. It therefore provides an abbreviation that can be used for every array in the class instead of the explicit statement of the 'old_'-variant.
The third extension concerns the return value of functions. It can be accessed by the variable 'result', provided the method has not been declared as 'void'. It may be used in the method body and in the postcondition.
The following grammatical rules describe their syntactic function. They are based on the LALR1-grammar of the official Java language specification ([GJS96]). A large part of the rule given here is also used in the further sections by the language extensions introduced there.
top of page 
table of contents
MethodBodyBlock:
{ [RequireClause] [BlockStatementList] [EnsureRescueClause] }
RequireClause:
/** require [BooleanAssertionList] **/
EnsureRescueClause:
/** EnsureClause RescueClause **/ /** **/
| /** EnsureClause **/
| /** RescueClause **/
EnsureClause:
ensure [NoChangeAssertionList]
NoChangeAssertionList:
NoChangeAssertion
| BooleanAssertion
| NoChangeAssertionList ; NoChangeAssertion
| NoChangeAssertionList ; BooleanAssertion
NoChangeAssertion:
nochange
BooleanAssertionList:
BooleanAssertion
| BooleanAssertionList ; BooleanAssertion
BooleanAssertion:
[AssertionLabel] BooleanExpression [{ MethodInvocation }]
BooleanExpression:
Expression
AssertionLabel:
Identifier :
The grammatical rules describe the method body which is now able to include a precondition and a postcondition apart from a sequence of statements (the 'StatementList'). These are documentation comments and contain a sequence of boolean assertions. In the postcondition the key word 'nochange' is allowed as well. Labels consist of an identifier which, separated by a colon, precedes a boolean assertion. This slightly odd way of handling the postcondition is necessary for the avoidance of conflicts in the grammar. The 'RescueClause' will be discussed in 2.5 The rescue-block: 'rescue'.
The following example (and those given later as well) shows an extract from the class 'Stack'. Preconditions and postconditions are described by using the examples of 'empty' and 'pop'. As the example in intended to be easy to survey some deletions have been made which have been marked '...'. '' denotes the method body that lacks some of the last statements. These are necessary for he explanation of the objects and have been made explicit. The interface 'Value' represents those objects that can be put on the stack, and the class 'Linkable' is used for the internal representation of the list elements.
public class Stack {
private Linkable root;
private int nb_elements;
...
public boolean empty()
throws RuntimeCheck.AssertionException {
if (nb_elements==0)
return true;
else
return false;
/** ensure result==(nb_elements==0); nochange **/
}
public Value pop()
throws RuntimeCheck.AssertionException {
/** require !empty() **/
<Beginn des Methodenrumpfs>
return x;
/** ensure nb_elements == old_nb_elements-1 **/
}
...
}
The precondition 'not empty' stated in the method 'pop' expresses the fact that this method may only be called if the stack is not empty. The postcondition of 'empty' ensures that its call does not cause any changes.
The postconditions of 'pop' ensures that each time it is called the number of elements decreases by one.
If the check is turned on during runtime the precondition and the postcondition are checked at the beginning and the end each time the method 'pop' is called. This is also the case if 'pop' was used within an assertion. If the check is turned on, the developer can be sure the condition is satified.
If one of the assertions is violated, an exception is triggered depending on the translationmode. In Java there are two kinds of exceptions, a checked one and an unchecked one. The checked ones are used in the mode 'CheckedContract'. In Java such a checked exception must be caught in any case. The Java compiler controls this in the translation. If in a method a checked exception can be triggered, this statement must be locked in a 'try-catch'-block or it must be passed over by a 'throws'-statement in the method head.
Like Java, JaWA is an object-oriented language and supports inheritance and polymorphism. Also, methods can be dynamically overloaded. Therefore, one cannot be sure that if a method has been called it is actually executed. The version of an inheriting class could be executed just as well. The contract that has been made by the method call must remain valid in any case. Therefore, according to the correctness formulae the precondition may be weakened and the postcondition may be strengthened only in the overloading method.If this is the case, the contract is also valid if the new version is dynamically executed.
Whether the assertions have actually been weakened or strengthened is something that cannot be proven in general. For finite codomains, as they are used for variables in computers, a check is possible but very tedious. In JaWA it is merely checked whether there are any assertions: if for a method no preconditions and postconditions, respectively, have been stated, the JaWA-precompiler checks if in the inheritance hierarchy an ancestor exists that has a method with the same signature. If in this method a precondition or a postcondition has been stated, an error message is generated and the translation is interrupted.
In each class a class invariant may be stated. This invariant contains assertions, that, apart from the parameter names, may be defined as in the preconditions of methods. The class invariant begins with the key word 'invariant' and is stated at the end of the class like a method.
The class invariant is supposed to include all assertions that contain conditions that hold for the whole class and not just for single methods. For instance, with their help the possible state space defined by the arrays can be restricted. In the example this is done for the array 'nb\_elements'.
The class invariant could also explicitly be added to each precondition and postcondition. The semantics would be the same, but its intention as an invariant condition could hardly be recognized. Moreover, class invariants, as opposed to preconditions and postconditions, are not inherited.
Like a method, the class invariant is declared at the end of the class and it is called by the other methods at the positions in which it is supposed to be checked. It too contains a sequence of boolean assertions in which the arrays and methods of the class can be used. Local variables and parameters cannot be used. The following grammatical rules describe their syntactic structure:
ClassBody:
{ [ClassBodyDecList] ClassInvariantClause }
ClassInvariantClause:
[InvariantClause]
InvariantClause:
/** invariant [BooleanAssertionList] **/
As can be seen from the rules in each class, at most one class invariant can be stated. The rule for the 'BooleanAssertionList' has already been described in 2.1 Preconditions and postconditions: 'require' and 'ensure'.
The following example shows the invariant of the class Stack, which contains a single assertion. It means that the number of elements, represented by the value of 'nb_elements', cannot become negative. The method 'pop' is used to illustrate the use of the class invariant.
public class Stack {
private int nb_elements;
private Linkable root;
...
public Value pop()
throws RuntimeCheck.AssertionException {
/** require !empty() **/
<Beginn des Methodenrumpfs>
return x;
/** ensure nb_elements == old_nb_elements-1 **/
}
/** invariant nb_elements>=0 **/
}
If the check of the assertion is switched on during runtime, the class invariant will be added to the precondition and to the postcondition by a logical 'and' and then checked. More precisely: at each method call from outside there are additional checks, i.e. at the beginning the class invariant will be checked in addition to the precondition, at the end the class invariant will be checked in addition to the postcondition.
The term "from outside" here represents a call in which a control flow 'enters' an instance, so to speak. An example shall illustrate this: Let there be two instances A and B of any, possibly the same class. A method a1 of the instance A is called which itself calls a method b of the instance B. And from b again a method a2 of the instance A is called. The calls a1 and b are both calls from outside, as the control flow leads from A via B back to A. Thus, the class invariant of the class of the instance A is checked only at a1 and that of the instance B only at b.
When using methods within assertions one has to pay attention to the fact that no cyclic calls are permitted. As this would result in infinite sequence of calls there would be a system crash. Note that during tests circles are found in any case if each method of each class is called at least once. A systematic test should always do this. Neither during the compilation nor during runtime is it checked whether the assertions actually make sense.
In Java there are three kinds of loops. They have been extended in JaWA by assertions. The loops are:
As loops can only be used within methods their assertions are not directly part of the documentation but they desribe the implementation. Therefore, they do not contribute to the contract between developer and user and should be formulated like ordinary comments.They do have an important function, however. They can reveal properties of the implementation that cannot be detected at first sight; in particular, the time limitation for loops can be shown. They thereby promote the understanding and help the developer formulate a precise precondition and postcondition or class invariant.
In the case of the forms discussed so far (the integration of assertions in the program code), it was implicitly assumed that the method call terminates and therefore returns to the caller at some point. This point of view is correct if loops are disregarded. With loops the time limitation has to be indicated explicitly, as otherwise the postcondition would never be checked and thus no guarantees as in a contract or in the form of a correctness formula could be given (see 1.2 Design by contract).
In JaWA an invariant and a variant can be stated in a loop. If, in the following, confusion with the class invariant cannot be excluded by the context, we use the expression "loop invariant". This invariant states an assertion that must be influenced by the execution of the loop, while the variant denotes an integer expression that explicitly has to do this. Two conditions are linked to the variant: first, its value has to be positive all the time, second, this value must decrease every time the loop is repeated. The Java-precompiler checks these conditions; as both conditions cannot be maintained infinitely long, the loop has to terminate.
The syntax of the invariant is the same as that of class invariants. After the key word 'invariant' a set of assertions, separated by semi-colon, can be stated. The variant consists of the key word 'variant' and an expression that yields an integer.
There now follow the grammatical rules for the while-loop and for the assertions mentioned above. The rules for both assertions are also used by the other types of loops.
WhileStatement:
while ( Expression ) AssertionClause
WhileStatementNoShortIf:
while ( Expression ) AssertionClauseNoShortIf
AssertionClause:
[InvariantClause] [VariantClause] Statement
AssertionClauseNoShortIf:
[InvariantClause] [VariantClause] StatementNoShortIf
InvariantClause:
/** invariant [BooleanAssertionList] **/
VariantClause:
/** variant IntegerExpression **/
In the Java grammar of the language specification two rules for the while-loop are needed in order to solve the dangling-else-problem of the if-then-else-statement (see [GJS96], page 259).
In the method 'push' of the class 'Stack' a while-loop is used, to run the list of stack elements:
public void push(Value x)
throws RuntimeCheck.AssertionException {
...
Linkable aktual=root;
int i=1;
while (i<nb_elements)
/* invariant nb_elements = old_nb_elements */
/* variant nb_elements-i */
{
<Beginn des Schleifenrumpfs>
i++;
};
...
}
The number of elements of the stack is used as an invariant. A termination condiction is stated here as well. It must not be changed by the loop. The local variable 'i' here matters as well, so that 'nb_elements-i' can be used as variant. Since the class invariant ensures that 'nb_elements' is not negative and that it is not changed by the loop, the value of the variant is positive due to the initialization of 'i'. In the loop body 'i' is always incremented by 1, but it remains less than 'nb_elements' as otherwise the termination condition would be fulfilled. The value of the variable thus decreases every time the loop is iterated but it never becomes negative, since the execution of the loop is stopped before. The time limitation is thus demonstrated.
The do-loop in Java is very similar to the while-loop. An termination condition is stated here as well. However, this condition is put at the end of the loop. The do-statement is thus executed at least once in any case. The grammatical rule for the do-loop is as follows:
DoStatement:
do AssertionClause while ( Expression ) ;
In the example class 'Stack' no do-loop is used. For this reason, the while-loop of the method 'push' shall here be presented in a do-loop with a similar meaning. As the do-statement is executed at least once in any case, a conditional statement was placed in front of it. The invariant and the variant are not changed. The meaning is not the same, though, as in the case of an unsatisfied condition of the if-statement the invariant is not checked. This is, however, irrelevant for the statements made here.
public void push(Value x)
throws RuntimeCheck.AssertionException {
...
Linkable aktual=root;
int i=1;
if !(i<nb_elements) {
do
/* invariant nb_elements = old_nb_elements */
/* variant nb_elements-i */
{
<Schleifenrumpf>
} while (i<nb_elements);
};
...
}
The for-loop in Java was taken over from C++. It has three expressions in the loop head that are separated by semi-colons: the initialization, the termination condition, and the updater. First, the initialization is executed. Then, the execution of the loop begins with the analysis of the termination condition. If it yields 'true', the loop body and then the updater are executed. Afterwards the termination condition is checked again. If it yields 'false', the execution of the loop is stopped. This loop can be provided with both an invariant and a variant:
ForStatement:
for ( ForInit ; Expression ; ForUpdate ) AssertionClause
ForStatement:
for ( ForInit ; Expression ; ForUpdate ) AssertionClauseNoShortIf ;
As a result of the dangling-else-problem of the if-then-else-statement two rules are needed for the for-loop as well (see
\cite{GJS96}, page 259).
The example of the for-loop is a transformation of the while-loop from the method 'push' as well. The statement for the increase of 'i' has been taken from the loop body (that remains unchanged otherwise) and inserted into the loop head.
public void push(Value x) {
...
for (Linkable aktual=root,int i=1; i<nb_elements; i++)
/* invariant nb_elements = old_nb_elements */
/* variant nb_elements-i */
{
<Schleifenrumpf ohne die Anweisung 'i++;'>
};
...
}
The check-statement is used to state an assertion at any part of the program code of the method body. It shows that at this position the validity of the condition is expected, although the reason for this is not immediately obvious from the program code.
For instance, at some point in the program code let there be the assignment 'x=y/z'. The programmer is sure that at this position z never equals 0. For this reason, he does not want to check this, such a check being superfluous. The reason for a value unequal to 0 may be found at another, more distant, position in the program code, possibly even in another method.
Someone else who looks over the whole code and who cannot recognize the reason immediately, is likely to assume that a mistake has been made or at least that the programming has been done rather sloppily. And even the programmer himself cannot always be aware of every single detail of the whole system and may want to be reminded of this important property. The check-statement formulates it explicitly: 'check z!=0;'. Of course, the check-statement can also be checked during runtime.
Instead of the check-statement one could also insert a comment or a statement which can be used to switch on the debugging. The result would be the same in the latter case. The check-statement should therefore be understood as a debugging statement that has the function of a comment (its syntax fitting the previous statements for the contract metaphor). It is constructed according to the following rules:
Statement:
StatementWithoutTrailingSubstatement
| LabeledStatement
| IfThenStatement
| IfThenElseStatement
| WhileStatement
| ForStatement
| CheckStatement
| RetryStatement
CheckStatement:
/** check [BooleanAssertionList] **/
As an example, consider a class in which a division by zero can be carried out. For this purpose, the class has a private method 'Div' which is called by the other methods of the class and performs the division by zero on the arrays x, y, and z.
class Alpha {
int x,y,z
...
private void Div()
throws RuntimeCheck.AssertionException {
/* check z!=0 */
x=y/z;
}
...
}
Assume that it is clear from the context in which 'Div' is used that the divisor z never equals 0. For someone who is not familiar with the implementation this information is hard to understand, as it is distributed over several methods. This is why it was explicitly formulated as a check-statement.
By stating a rescue-block the integrity of the respective instance can be secured in the case of a violated exception. A detailed description of the aims of its use is given in 1.6 Violations of the contract: success or failure. It is usually used by the rule 'EnsureRescueClause' (see section 2.1 Precondiitons and postconditions: 'require' and 'ensure', that means at the end of the method, after the postcondition and before the close brace. It consists of a sequence of catch-statements which each contain a block with statements.
RescueClause:
rescue [CatchList]
CatchList:
Catch
| CatchList ; Catch
Catch:
catch ( Expression ) Block ;
The 'Expression' denotes, for instance, an expression 'MyException' by means of which all all exceptions of the class type 'MyException' or one of its descendants can be caught. The statements in the 'Block' are therefore changed accordingly.
As an example, consider the method 'Div' used in the description of the check-statement. A rescue-block has been added to it that sets the array x on 0 in the case of an exception due to a violation of the check-statement. In the example, this array shall maintain the integrity of the respective instance of the class Alpha.
class Alpha {
int x,y,z
...
private void Div()
throws RuntimeCheck.AssertionException {
/* check z!=0 */
x=y/z;
/** rescue catch (RuntimeCheck.AssertionException e)
{x=0} **/
}
...
}
In Java each assertion that can trigger a checked exception must be surrounded by a try-catch-finally-block. In the try-block it is triggered and it is caught again in the catch-statements. The catch-statements are stated by the programmer in the rescue-block, the try-block is generated by the JaWA-precompiler in the respective translationmode.
Each catch-statement has a parameter under which the caught exception classes can be referenced in its block. The block of the first catch-statement fitting the exception is executed. The Java-compiler ensures that for each exception that can be triggered in a try-block such a statement exists.
On the basis of the extensions made so far, each violation of an assertion leads to the triggering of an exception which is passed over method by method (corresponding to the call sequence) and which finally leads to the termination of the system. By a retry-statement this chain is interrupted. Instead of passing over an error the method is executed again. In this way the original aim can possibly be achieved; at least the state remains consistent.
The retry-statement that makes this possible has already been discussed in section 1.6 Violations of the contract: success or failure. It can be used in JaWA like an ordinary statement (though only within the blocks of the catch-statements) according to the following rule:
Statement:
StatementWithoutTrailingSubstatement
| LabeledStatement
| IfThenStatement
| IfThenElseStatement
| WhileStatement
| ForStatement
| CheckStatement
| RetryStatement
RetryStatement:
retry
To illustrate the application of the retry-statement, the example of the method 'Div' will be used again. In contrast to the example in the rescue-block, the value of the divisor is changed here and the method is executed once again.
class Alpha {
int x,y,z
...
private void Div()
throws RuntimeCheck.AssertionException {
/* check z!=0 */
x=y/z;
/* rescue catch (RuntimeCheck.AssertionException e) {
z!=1; retry
}
*/
}
...
}
The method body is started again (under different conditions) by the retry-statement in case an assertion of the check-statement is violated. As in Java local variables are declared within the block itself, changed conditions between two runs can only be stored in arrays of the class.
Each assertion, except for the loop invariant, is a boolean expression the validity of which can be checked in a conditional statement with a preceding negation operator. This negation triggers an exception if the assertion condition is invalid.
The precondition and the postcondition are changed at the beginning and at the end of a method call, respectively. If in the postcondition a variable with 'old' is used, after the precondition a local variable is generated that temporarily stores the value. If 'nochange' is used, this is done for all attributes of the class, no matter if they are defined as 'private', 'protected', 'public', or without modifier.
The class invariant is translated into a new method which is called from the preconditions and postconditions if and only if a call is made from outside (see section 2.2 The class invariant: 'invariant').
For this purpose a call counter is used that is incremented by 1 within the precondition and decremented by 1 within the postcondition. If the ancestor of a class has a class invariant it is called as well.
With loops the invariant is checked at the beginning of each run and directly after a conditional statement. A local variant is generated for the variant. It temporarily stores the value at the beginning of a run such that it is possible to check at the end whether its value has decreased and whether it is still positive. The check-statement is locally expanded like a macro. A conditional statement for the check of its assertion is directly generated from it.
As a result of the language extensions there are a few limitations for one's own programs.
The key words 'require', 'ensure', 'invariant', 'variant', 'check', and 'nochange' have been added to the grammar by the extension. Although no problems can be expected at this point, they are not supposed to be used as identifier. They may in no case occur as the first word at the beginning of documentation comments, because otherwise they would be interpreted as assertions and parsed.
In the methods the following local variables are used depending on the assertions:
The arrays added by the precompiler and the local variables should only be accessed by the statements generated by the compiler. They are not meant to be used in the main program, but this cannot be prevented. Such a use may render the assertions ineffectual. In this way the check of the class invariant would be carried out at completely wrong points in time because of a change of the array 'depthOfCall' not provided for.
In contrast to Eiffel in the approach developed for Java the class invariant is only checked in the case of method calls; it is not additionally checked when public variables are accessed. This kind of access is done from outside and should lead to check of the class invariants. However, the implementation by a precompiler would be rather arduous as each simple variable access would have to be replaced by a method call.
For this reason, a compromise is suggested here that takes both aspects into account. When with an attribute a violation of the invariant may occur as the result of a value assignment, the attribute is considered critical. Such an attribute should be declared as nonpublic as they would violate the principle of data encapsulation. Access to them should always be encapsulated via a method. The uncritical attributes may remain public to increase the efficiency. This also applies to arrays which are declared as class attributes, as they are only set up once for all instances of a class. In this case one instance might violate the invariant of another.
The array 'depthOfCall' is declared as type integer. The maximal depth of call is therefore restricted by the codomain 'Integer'. This also applies to the number of loops of a method body, as the local variable 'variant' is numbered consecutively (for the purpose of discrimination).
The rescue-block and the retry-statement can be used to satisfy (by another try) the postcondition (and the class invariants). They can also be misused, however, namely by changing the values of arrays or the return value in such a way that there is a discrepancy to the expected results. In section 2.6 The retry-statement this was done for the method 'Div'. However, in this way the proper computation was evaded. Even though the method was terminated successfully, it now yields a value that is in no way related to the result of the computation. The developer himself has make sure that he does not overlook the gist of language extensions.
The installation is described in the file 'Install.txt' in the superordinate directory.
In the first, basic, step it is attempted here to achieve a pure description of the class that is independent of the implementation idea. This description should present a general and reusable solution of the problem and thus exceed the momentary needs. For our example of the concatenated list this implies that any element can be included in the list and that useful services like 'inserting' and 'deleting' exist. As lists are very general, only a small number of preconditions and axioms can be formulated. The ADT is called List'. The data objects are represented by the set 'Value'.
ADT List
TYPES
List, Value, BooleanFUNCTIONS
new : ---> List empty : List ---> Boolean insert : Value x List ---> List delete : List -/-> ListPRECONDITIONS
For all l:List: delete : pre delete(l) = not empty(l)AXIOMS
For all v: Value and l:List: empty(new()) not empty(insert(v,l))
In the second step it is tried to describe the ADT by a class. This class is also called 'List' (for ADTs and their functions 'italics' are used, for classes and their arrays 'nonproportional') script. The aspects of 'representation' and 'active machine' come into play here as well. For the representation another class 'Linkable'shall be used. It provides list elements that can each include one data object and a reference to the following list element. A list is thus a concatenation of list elements the root of which is stored in the instance of 'List'. For the representation of the data objects the ADT 'Value' is defined as an interface 'Value'. Both classes and the interface are inserted in the package 'DataContainer'.
The aspect of the active machine is realized by means of a cursor (in which the instances store the current working position). At this position elements are then inserted or deleted. A cursor allows for methods with few parameters and for a very efficient implementation. If, for instance, several elements are deleted in the middle of the list in a row, the list does not have to be run through again up to the corresponding position for every element. Also, search operations like 'FindFirst' and 'FindNext' can be implemented which would not be possible without internal state.
One should make a decision for a translationmode at this stage already, as in the mode 'Contract' all exceptions that can be triggered within their bodies have to be stated in the method heads.
The following listing shows an extract from the class 'List', which is stored in the directory 'DataContiner' in the file 'List.JaWA'. It is translated by the compiler into the file 'List.java' which then only contains Java-statements. The compiler then generates the file 'List.class'.
Most of the methods and assertions have only been included in the class by virtue of the representation. The precondition stated in the ADT for the function 'delete' is used in the method 'Delete'. The first axiom of the ADT is implicitly used in the constructor, the second in the postcondition of the method 'Insert'.
package DataContainer;
public class List {
private Linkable root;
private Linkable cursor;
private int pos;
private int nb_elements;
public boolean IsEmpty()
throws RuntimeCheck.AssertionException {
return (nb_elements == 0);
/** ensure result == (nb_elements==0); nochange **/
}
public void GoToFirstElement()
throws RuntimeCheck.AssertionException {
/** require !IsEmpty() **/
...
/** ensure nb_elements==old_nb_elements **/
}
public void GoToNextElement()
throws RuntimeCheck.AssertionException {
/** require !IsEmpty() **/
...
/** ensure nb_elements==old_nb_elements **/
}
public void GoToLastElement()
throws RuntimeCheck.AssertionException {
/** require !IsEmpty() **/
...
/** ensure nb_elements==old_nb_elements;
cursor.GetNext()==root
**/
}
public void GoToPrevElement()
throws RuntimeCheck.AssertionException {
/** require !IsEmpty() **/
...
/** ensure nb_elements==old_nb_elements **/
}
public void Insert( Value value )
throws RuntimeCheck.AssertionException {
/** require value!=null **/
...
/** ensure !IsEmpty() **/
}
public void Delete()
throws RuntimeCheck.AssertionException {
/** require !IsEmpty() **/
...
/** nb_elements==old_nb_elements -1 **/
}
/** invariant 0<=pos; pos<=nb_elements;
pos==GetPosition(cursor);
cursor==null | pos!=0 ;
**/
}
After the class has been described and all methods have been implemented, the third step consists in the translation. As already mentioned, the translationmode 'Contract' shall be used. For this reason, all calls of methods of the class 'List' have to be surrounded by a try-catch-statement.
In order to use the class 'List', the following brief example was defined 'X', which represents an executable Java-progam. The class 'x'implements the interface 'Value'.
package DataContainer;
class X implements Value {}
public class TestList {
static List l;
public static void main(String[] argv) {
try {
l = new List();
x= new X();
l.InsertAfter(x);
} catch (RuntimeCheck.AssertionException e)
{System.out.print("ERROR");}
}
}
When the precompiler has been installed, the translation of the class 'List' can be started by the instruction:
JaWA DataContainer/List.JaWAAfterwards the test program is translated by the instruction:
JaWA DataContainer/TestList.JaWAAs it contains no assertions, the ordinary Java-compiler could have been used at this stage just as well. The instruction:
java DataContainer.TestListexecutes the Java-Virtual-Machine, which loads the classes and executes the program.
The check of the assertions during runtime makes it possible to find and localize errors in one's own software. However, this requires some time and also some memory, depending on how intensively one has worked with assertions. If efficiency is regarded as more important, this is annoying and not acceptable. But it is equally annoying to renounce the advantages of design by contract (like debugging, rescue-blocks, etc.) in favour of efficiency.
Both the Eiffel-compiler and the JaWA-precompiler try to generate software that can be used in practice. For this reason, the options used in the Eiffel-compiler for the selection of the assertions to be checked have been transferred to the JaWA-precompiler. There are three modes:
In the All-mode the check is carried out for all assertions stated in the program. In case they are violated exceptions are generated and the control is handed over to the rescue-block, or, if this does not exist, to the caller. A checked exception has to be, an unchecked exception can be caught.
At the beginning of the development the All-mode should be used in order to detect errors as soon as possible (this applies to both those errors that refer to the general conception as such and to those that refer to the way the implementation is done). If after thorough testing one feels secure that no or not many errors are left, the extent of the checks can be controlled by one of the other modes or by a more efficient execution.
In the preconditions-mode it is only the preconditions of method calls that are checked and that trigger exceptions. If a slightly slower runtime (about 2o%) is acceptable, the option Preconditions should be used. It represents a compromise between efficiency and security: only the preconditions (but not the invariants) of the methods are checked.
In the Nothing-mode the check of the assertions during runtime is completely switched off. Thus, assertions cannot be regarded as guarantees anymore. If there were a violation, it would not be detected which could have far-reaching consequences. It is as if there were no assertions: the integrity of the system may get lost and the system may crash as well.
The example for the check-statement in section 2.4 The check-statement illustrates these consequences. The assertion guarantees that z is not equal to 0. If this check is not carried out, z may cause a runtime error in the next division which may result in a system crash. The same applies to empty references.
Consequently, if one chooses the option Nothing one should really make sure that the system works properly .
The switch to the new concept requires some changes in the development of software systems. A slow and gradual transition should be possible. For this purpose, four different translationmodes have been integrated by means of which the developer can control to wthat extent the concept is used. This is also relevant for cases where the concept shall be included into already existing systems later on. The translationmodes do not only facilitate an increase in efficiency but also the step by step initiation into the usage of assertions and the precompiler. Here are the modes:
The translationmode Nothing is the first mode. It allows the addition of assertions as comments and exerts no influence on the behaviour of the system at all. This mode is meant to make the first two aims of design by contract possible: a formal specification and its automatic incorporation in the documentation.
Although this mode does not change the system in any way and can therefore be inserted into already developed and used programs later on, it can be regarded as a big step on the way to a new concept, namely the methodical switch. This mode is meant to enable one to experience the formal description of objects by ADTs without forcing the user to change his behaviour with respect to the implementation. Hopefully, then, the change does not become too extensive.
At the same time, the mode offers a certain security. If programs are nor error-free in principle, the JaWA-precompiler isn't either. With the help of this mode it becomes possible to easily and quickly switch off the precompiler so that problems at this stage are avoided. In this way, the arduous work of changing makefiles and the manual renaming of the sources files (to 'name.java') is avoided.
This mode should not be used if efficiency is required in the execution, as in this mode the translation is disabled. Thus, possibly existing rescue-blocks would not be translated either. These can however be used for exceptions that have not been triggered by assertions. For higher efficiency the checkmodes 'Nothing' or 'Preconditions' should be used. Of course this should not be done till the end of an extensive test phase. The developer ought to be sure the system does what he wants.
The warning-mode makes it possible to check the assertions during runtime. This mode therefore extends the first one by the debugging-functionalities. The control flow of the program is not changed but an instance of the class stated in the configuration file under 'WarningClass' is generated and its method 'Message' is called. This class is no exception. By means of this mode the work done in the first (the formal specification) is meant to be made checkable.
The next step is the UncheckedContrakt-mode. In this mode the translation of the assertions is carried out so that they can trigger exceptions when violated. However, an unchecked exception is used. Such an exception may be caught but does not necessarily have to. As an exception that has not been caught leads to the termination of the system, the developer has to make sure that at this place in the system no problems can occur.
In this mode the linking to the exception handler is carried out and fault-tolerant behaviour is made possible. Up to this mode a switch between the modes is possible without any particular efforts; it can thus be included in already existing projects quite unproblematically.
The Contract-mode works like the previous mode, but uses checked exceptions. It thus establishes the contract between user and developer. Every statement that can throw an exception must be surrounded by a try-block. Every method that passes on a checked exception must declare the latter in its head. As the precompiler is not supposed to change the interface of a class, this must be inserted by the developer himself. A switch to this mode therefore involves changes in the class declarations and in the programs that call their methods as well. Still, this mode should be aimed at in the use of assertions, as only at this point can we really speak of design by contract.
The Java-compiler is called from the JaWA-compiler in order to check the semantic correctness of the intermediate form 'Check' and to translate the JaWA language extensions. Both tools must configurable. Therefore, all parameters which have to be stated at the call of the JaWA-precompiler are passed on to the Java-compiler such that the latter can still be set.
For the time being, these settings are stated in a configuration file called 'JaWA.rc'. The JaWA-precompiler searches for this file in the current directory first. If it cannot find it, it searches in the user's home directory. If the configuration file still isn't found, the default settings will be used for the options.
The following list contains all options and possible values. These values are separated by a comma; the default setting is printed in 'italics'. If any string of characters may be used, this has been indicated by '...':
VerboseMode = on , off
Logfile = ./JaWA.log , ...
CheckMode = Nothing , Preconditions , All
TranslationMode = Nothing , Warning,
UncheckedContrakt, Contract
ExceptionClass = RuntimeCheck.AssertionException , ...
RuntimeExceptionClass = RuntimeCheck.AssertionRuntimeException , ...
WarningClass = RuntimeCheck.Warning , ...
If the VerboseMode is switched on, control ouputs are generated by means of which it is possible to retrace what the JaWA-precompiler is doing. This mode is not meant to be used for the debugging of the precompiler, but it serves the purpose of checking if a configuration file has been used and if so, which one. It also shows which part is currently being translated.
If a logfile Logfile is stated, the debug output and the verbose output are both directed into the respective file, otherwise they are directed into the standard output. Nromally, the file 'JaWA.log' is generated in the current directory.
The checkmode CheckMode defines which assertions are supposed to be checked.
The translationmode TranslationMode defines the way in which the assertions are handled.
In ExceptionClass the class for checked exceptions that is supposed to be used in the translationmode 'Contract' can be stated. Therefore, this may also be an extended class of its own, which, for instance, makes the error message appear in a special window or which saves it in a data base. The class stated here has to inherit from the class 'AssertionException' from the package 'RuntimeCheck'.
In RuntimeExceptionClass the class for unchecked exceptions to be used in the translationmode 'Contract'can be stated. It must be a descendant of the class 'AssertionRuntimeException' from the package 'RuntimeCheck'.
In WarningClass the class for the output of information on violated assertions that is to be used in the translationmode 'Warning' can be stated. It must inherit from the class 'Warning' from the package 'RuntimeCheck'.
The following list shows all error messages generated by the JaWA-precompiler. It is divided into errors occurring during the compilation and and errors occurring during the execution of the JaWA program.
The following list shows all error messages generated by the precompiler. If alternatives are possible in the messages, these have been put into parentheses and separated by commas.
The following list shows all runtime error messages. They are determined by the classes stated in the configuration file. If the default settings are used, the following two-line message is given (as with the Java-compiler):
" 'filename':'line': 'message' in class 'c' method 'm'
'filename':'line': 'label' 'assertion' "
where 'filename' stands for the name of the source file, 'line' for the line number, 'c' for the name of the class, 'm' for the name of the method, 'label' for the optional label of the assertion, 'assertion' for the assertion itself and 'message' for one of the following messages:
This section contains some references to further sources of information.
LINKS:
Bibliography: