Dynamic Analysis - Assertion Checking
CIS 841
Summer '98
Peter Chung
Eric Fisher
Fredrik Simonet
Developing and testing a software system is a costly and time-consuming job. This paper will discuss a development method that improves correctness and robustness of the software. Assertions provide a method for documenting and dynamically debugging the software at run time. Assertions are Boolean expressions used in preconditions, postconditions, and class invariant. Applying preconditions and postconditions to a routine effectively creates a contract between the class and the client. Thus, "Design by Contract" is often associated with assertions. Additionally, there are many software development tools that support assertions and allow runtime evaluation of the conditions. This paper describes the method of using assertions to improve software correctness and briefly discusses some of the software tools that are available.
2. Introduction
A common practice in software development is to have extinctive testing, validation and verification to find program faults. Debugging only find failures after it occurs. Having assertions in the program is a testing technique that will reveal defects early in the development process. Assertions are functions that evaluate to "true" when a program state is satisfied and "false" otherwise. Assertions can be monitored at run-time, making it a powerful debugging tool. Assertions can also be used to document and implement specifications, thereby facilitating the software development. Developers use assertions to expedite software debugging during development. In addition, adding assertions to the program may find faults where test cases are ineffective.
There are three types of assertions: precondition, postcondition, and class invariant. The precondition describes the properties that must hold true whenever the method is called and the constraints that must be satisfied for the method to function correctly. The precondition is evaluated at the entry point of the method. This often helps detach errors for the least amount of processing overhead. The postcondition describes the properties that the method guarantees when it returns. The postcondition is evaluated at all exit points of the method. Invariant is a statement about a class. It is always true for all instances of the class. The invariant is evaluated at the entry and exit points of all public methods in a class. Invariant may become false during execution, but must be restored to true by the method returns. Class invariant is implicitly ANDed to both precondition and postcondition of every method.
Assertions are used to improve the correctness of the software. That is, to reduce the discrepancies between the specification and the implementation. Assertions are expressions that state what a method must satisfy, without specifying the exact implementation. By including formal constraints on the software's behavior in the source text, it lowers the risk of discrepancies between the specification and implementation. These constraints do not have to include every aspect of the specification, but more importantly it should entail the interface requirements. In a recent study performed by Perry & Evangelist [10], it was found that most software faults are interface faults. Therefore, including assertions in methods will reduce interface faults.
Assertions are supported in many development environments today. There are programming language like Eiffel [8] and Turing [6] that include assertions as part of the language definition. Other languages such as C, C++, and Java supply minimal or no support at all for dynamic assertion checking. In these cases, a preprocessor like APP [5] or Nana [11] is used to convert annotations in the source file. The tool we investigated was AssertMate [12], for Java. Since Java does not provide a mechanism for assertions, AssertMate provides both a preprocessor and the classes for run-time assertion checking in Java. In all these environments, the assertions can be optionally configured at run-time to determine how assertion violations are handled and how much checking will be performed.
Assertions are basically simple predicates. Most assertion tools/languages support only basic features of predicate calculus. They all provide simple logical expressions (i.e. AND, OR, NOT) and basic arithmetic. The more advance environments provide the universal and existential quantifiers over a defined domain. Since these quantifiers are usually implemented with loops, the domain has to be restricted. In languages that rely on preprocessor, the assertions are usually written inside the comment section using extended comment indicators. APP's uses the following syntax: /*@ expression @*/, while AssertMate uses /*+ expression +*/. Languages like Eiffel or Turing have keywords built into the language for each type of assertion. All of the development environments mentioned above support the use of preconditions and postconditions. More advanced environments support class invariance, loop invariance, and intermediate data assertions. These latter constructs are used to place constraints on the data internal to the method, rather than just on the interface to the method.
3.1. What is Precondition?
A precondition is a Boolean expression used to check the properties of the program or input variables at the entry point of public methods. It defines the constraints in which the method will operate properly. Typically, the precondition is the first statement in the method.
The following section of Java code uses AssertMate notation is the constructor for the Banking example. There are two preconditions specified. The first precondition, "!user.equals("")", ensures a user name is given when the constructor is invoked. The second precondition, "amount >= 0", ensures the user is not trying to open a banking account with a negative starting balance. The second precondition is an obvious constraint on any banking system. However, many times the obvious constraints are over looked. Therefore, the second precondition is needed.
public Banking(String user, float amount) {
/*+ PRE_CONDITION (! user.equals("") , "Invalid User name"); +*/
/*+ PRE_CONDITION (amount >= 0 , "Invalid starting balance."); +*/
owner = user;
balance = amount;
}
Figure 1: Banking Example Constructor.
3.2. What is Postcondition?
A postcondition is a Boolean expression used to check the return value of the method. It ensures to the caller of the method that the class property is satisfied upon return from the called method. This allows for proper continuation of the program. The postcondition is checked at every return point of the method to ensure the method will result in a valid state for the caller, no matter which path of the method is executed. Therefore, postconditions need a rich assertion language to be able to handle these conditions. Typically, the postcondition is placed immediately after any precondition statements.
The following section of Java code uses AssertMate notation is the deposit method for the Banking example. This method has one postcondition, "balance == (OLDbalance+amount)". This postcondition ensures the new balance of the account equals previous balance increased by the amount deposited. Otherwise, money can be lost during the deposit transaction. In the example, the calculation is simple, "balance += amount". However, in a more complex system, the postcondition serves as an invaluable tool to check for correctness.
public void deposit( float amount) {
OLDbalance = balance;
/*+ PRE_CONDITION(amount >0 ,"Invalid deposit amount."); +*/
/*+ POST_CONDITION(balance == (OLDbalance+amount),"Invalid balance calculation."); +*/
balance += amount;
}
Figure 2: Banking deposit method.
3.3. What is Class Invariant?
A Class Invariant is a Boolean expression used to define the valid properties of correctly. The user of the class can be guarantee the class properties are satisfied. It defines all the properties in which the class can operate. Class Invariants are implicitly ANDed with the all preconditions and postconditions. Typically, the class invariant is placed in the global variable section of the class definition, see Figure 3.
The following section of Java code uses AssertMate notation is the Class definition for the Banking example. This example has one class invariant, "balance >= 0". This ensures that the balance of the account will always be greater than or equal to zero. At this time, AssertMate does not provide support for class invariant. Therefore, the ASSERTION clause needs to be place manually before and after the call of all public methods, see Figure 4.
public class Banking {
private float balance = 0;
private float OLDbalance = balance; // Need only to check the
// postcondition.
private String owner;
/*+ ASSERTION(balance >= 0 ,"Invalid Account Balance."); +*/
. . .
}
Figure 3: Banking Class Definition.
. . .
/*+ ASSERTION(balance >= 0 ,"Invalid Account Balance."); +*/ bank.balance(amount); /*+ ASSERTION(balance >= 0 ,"Invalid Account Balance."); +*/
. . .
Figure 4: Class Invariant checking in AssertMate
3.4. What is Design by Contact?
Design by Contract describes a method and philosophy for developing software. As in personal affairs, a contract obligates two parties to certain rules that constrain and hopefully benefits both parties. Design by Contract does the same for software development. It states what are the responsibilities of the class designer and what are the responsibilities of the developer calling that class. When it is not specified who is responsible for checking the data passed between routines, both the calling and the called method will perform data validation. This redundancy leads to more complex code, increasing the risk for errors and complicating software maintenance.
The approach taken in Design by Contract is to use preconditions and postconditions to specify the constraints for that method. These constraints bind the method to the caller. When calling a method, it is the responsibility of the caller to satisfy all the precondition of the method. Before returning from the method, it is the responsibility of the class developer to guarantee all postconditions are satisfied. The advantage for the developer of the class is that the input conditions to the routine are assumed to be correct. The checking had to have been done, by the client. This will allow the developer to focus only on the implementation. For the client, the benefit is the guarantee of correct results upon return from the routine.
3.5 Handling Assertion Failures
Assertions are usually checked during debugging and testing. It is recommended to include assertions throughout the program. Based on the specification, all the preconditions for the method should be identified and implemented as assertions. In addition, postconditions should also be defined as assertions to capture as much information as possible about the class property prior to returning from the method, whether it is a change in state or a change in value for a variable. With assertions in place, assertion violations can be detected at run-time.
When an assertion fails, there are four (4) ways to handle them. First, a good default behavior is to terminate the program. This is the safest and perhaps the most desired result. However, this may not be good enough for debugging purposes. The next alternative when an assertion failure is to stop or halt the program into a suspended mode for debugging. This allows the developer to determine the nature of the assertion failure. A third choice is to allow the program to continue and examine the propagation of the error. Assertions added to a program increase the ability to detect error propagation. This is desired because it reduces the probability of hiding an error that may be inadvertently corrected. In other words, a reduction in error masking occurs. Therefore, errors are more likely to be found during testing. Finally, on an assertion failure, an error handling routine could be implemented to throw an exception. The error handling routine is defined by the developer as needed. For example, the developer could define an error handling routine to output an error message to a log when an assertion failure occurs.
4.1. Overview
AssertMate gives Java users the ability to perform assertion checking as found in other Object-Oriented programming languages. Java does not have any support for assertion checking built into it, unlike C++. Therefore to support assertion checking in Java, an external tools is needed. AssertMate provides the basic assertion checking functionality for Java in a customizable and developer friendly manner. It uses the extended comment indicators "/*+ ... +*/" notation to insert the assertion command into the code. When the assertion clauses are needed, the AssertMate preprocessor needs to executed on the Java code before the Java compiler compiles it. This is a one step process that can be incorporated in a makefile. After debugging, the code can be compiled without the use of the preprocessor.
AssertMate support the following assertion constructs:
<expression> is a normal Java expression, which will evaluate to true or false. <message> is the message displayed when the assertion fails. A stack trace and the assertion type will also appear if the assertion fails to help in the debugging of the program. By default, AssertMate prints all messages in a popup window. Then, it terminates the program. As an option, the messages can be redirected to the standard output and the program can continue to run when an assertion fails. For these customization options, refer to the AssertMate documentation.
4.2. Limitation
AssertMate makes great advancement in assertion checking for Java. It provides a preprocessor to overcome Java's limitations and makes assertion checking customizable. However, AssertMate falls short in a number of ways. First, it does not support the use of the Global Invariant/Class Invariant. The Class Invariant should be checked before and after every public method in the class. It should hold true at all stable points of the class. Another area AssertMate needs improvement is the Boolean expression aspect on the clauses. It would be helpful if it support a richer assertion language commonly used in assertion creation, such as FOR ALL and THERE EXIST. This would make AssertMate more consistent with typical assertion checking languages.
4.3. Example
The following is any example of a Banking class using AssertMate. The Banking class consists of the following public methods:
The Global Invariant for this Banking class is the balance must be greater than zero.
The follow is the Java source code of the banking class include the AssertMate assertions in the "/*+ ... +*/" tags. To run the example, click the Demo button.
public class Banking {
private float balance = 0;
private float OLDbalance = balance; // Need only to check the postcondidtion.
private String owner;
////////////////////////////////////////////////////////////
public Banking(String user, float amount) {
/*+ PRE_CONDITION (! user.equals("") , "Invalid User name"); +*/
/*+ PRE_CONDITION (amount = 0 , "Invalid starting balance."); +*/
owner = user;
balance = amount;
}
////////////////////////////////////////////////////////////
public String getOwner(){
return owner;
}
////////////////////////////////////////////////////////////
public float getBalance(){
return balance;
}
////////////////////////////////////////////////////////////
public void deposit( float amount) {
OLDbalance = balance;
/*+ PRE_CONDITION(amount >0 ,"Invalid deposit amount."); +*/
/*+ POST_CONDITION(balance == (OLDbalance+amount),"Invalid balance calculation."); +*/
balance += amount;
}
////////////////////////////////////////////////////////////
public void withdraw( String user, float amount) {
OLDbalance = balance;
/*+ PRE_CONDITION(amount >0 ,"Invalid withdrawal amount."); +*/
/*+ PRE_CONDITION (owner.equals(user),"User is not owner of account"); +*/
/*+ PRE_CONDITION (amount <= balance , "Invalid withdrawal amount."); +*/
/*+ POST_CONDITION(balance == (OLDbalance-amount) ,"Invalid balance calculation."); +*/
if (! owner.equals(user))
return;
balance -= amount;
}
////////////////////////////////////////////////////////////
public void closeAccount( String user) {
/*+ PRE_CONDITION (owner.equals(user),"User is not ower of account"); +*/
/*+ POST_CONDITION (balance == 0 , "Invalid balance calculation."); +*/
if (! owner.equals(user))
return;
balance = 0;
}
}
Figure 5: Example of a Simple Banking Class with AssertMate assertions.
To run the above code in Figure1 with AssertMate:
See a Demo Demo Fixed.
Correctness - The conformance between a software specification and its implementation.
Assertions - A simple boolean expression that places constaints on the software's behavior.
Precondition - The properties that must hold true for the correct operation of a method or function.
Postcondition - The properties that a method or function guarantees upon exiting.
Invariant - A global property of a class that must be preserved by all methods, in that class.
6. References
7. Quiz
|
Num |
Question |
Answer |
|
1 |
What is a function or expression that evaluates to "true" or "false"?
|
|
|
2 |
A ________ is a global property of a class that must be preserved by all methods in that class.
|
|
|
3 |
A precondition is
|
|
|
4 |
Design by contract is
|
|
|
5 |
What is the benefit of design by contract?
|
|
|
6 |
A class invariant may become false during execution?
|
|
|
7 |
What is AssertMate?
|
|
|
Given the code segment, answer questions 8, 9 and 10.
|
||
|
8 |
What are the preconditions?
|
|
|
9 |
What are the postconditions?
|
|
|
10 |
What are the class invariants?
|
|
|
11 |
Preconditions are checked at the entry point and exit point of the method?
|
|
|
12 |
When are postconditions checked?
|
|
|
13 |
When are class invariants checked?
|
|
|
|
|
Date |
Eric |
Fred |
Peter |
|
6/2 |
0 |
0 |
2 |
|
6/3 |
6 |
6 |
4 |
|
6/4 |
6 |
4 |
6 |
|
6/5 |
3 |
3 |
3 |
|
6/6 |
0 |
0 |
0 |
|
6/7 |
1 |
1 |
1 |
|
6/8 |
0 |
0 |
0 |
|
6/9 |
3 |
3 |
3 |
|
6/10 |
1 |
1 |
1 |
|
6/11 |
2 |
2 |
2 |
|
6/12 |
0 |
0 |
0 |
|
6/13 |
2 |
4 |
1 |
|
6/14 |
0 |
0 |
0 |
|
6/15 |
5 |
7 |
5 |
|
6/16 |
5 |
7 |
5 |
|
6/17 |
|||
|
6/18 |
Time in Hours