 |
|
|
Abstract
The ability to think abstractly about the components of a computer program is critical for computer science students. A student who has not yet developed this ability tends to view a program as an unstructured collection of statements and expressions. Introductory computer science textbooks promote the use of pre-conditions, post-conditions, and abstraction functions as techniques for fostering abstract thinking. Existing programming languages and tools, however, do not generally support these techniques. Consequently, we have built and are beginning to experiment with Javiva. Javiva extracts pre-conditions, post-conditions, and abstraction functions ¾ included as stylized comments in Java source files ¾ and uses them to create instrumented class files. When these instrumented class files are run, they automatically diagnose and report violations by methods of pre-conditions and post-conditions. These classes also exploit abstraction functions to automatically produce abstract visualizations of the objects that are created by classes.
Motivation
The ability to think abstractly about the components of a computer program is critical for computer science students. A student who has not yet developed this ability tends to view a program as an unstructured collection of statements and expressions. Viewed this way, the complexity of a program grows exponentially with its size. As a result, such a student has difficulty moving beyond reading and writing toy programs. On the other hand, a student who has learned to think abstractly about program components tends to view a program as a much more easily understood collection of functions and classes. By thinking about functions in terms of what they do and about classes in terms of what they represent, such a student is able to cope with much larger programs.
Introductory computer science textbooks promote a variety of techniques that foster abstract thinking. The use of pre-conditions and post-conditions to specify the behavior of functions is widely advocated. The use of abstraction functions to help specify the meaning of classes is also promoted [1,2]. All of these techniques allow students to reason about the correctness of their programs, leading to the development of higher quality code. Existing programming languages and programming tools, however, do not generally support these techniques. As a result, the use of pre-conditions, post-conditions, and abstraction functions in student programs is typically confined to comments that are ignored by compilers, interpreters, debuggers, and (all too often) the students themselves.
The interactive debuggers that students use to develop their programs allow students to trace the execution of their programs on a statement-by-statement or function-by-function basis, to examine the values of variables as the program is running, and to invoke directly the functions of the program. Unfortunately, debuggers also advance the view of data as aggregates of primitive values and of programs as sequences of statements. Debuggers deal with such language-level constructs as loops and arrays; they do not deal with such program-level abstractions as sorting algorithms and sets. As a consequence, a student who wishes to use an interactive debugger to examine (for example) a set-valued variable will not be shown a set; he or she will be shown the internal representation of a set. The student must provide the mental mapping from the representation to the abstract value, and for many students this mapping is difficult.
Because programming languages and tools do not reinforce the use of pre-conditions, post-conditions, and abstraction functions, students tend to downplay their importance. We believe that direct language support for these abstraction techniques will encourage their use and reinforce their utility. Furthermore, such support will make possible a variety of powerful new debugger capabilities. All of this, in turn, will make it easier for students to learn how to write large programs.
Based on these beliefs, we have built and are beginning to experiment with Javiva, a preprocessor for the types of Java programs written by CS1 and CS2 students. Using Javiva, students are able to include pre-conditions and post-conditions for functions, and abstraction functions for classes, as stylized comments in Java source code. Javiva processes the comments to incorporate instrumentation into the class files that are produced by the Java compiler. When these instrumented class files are used at runtime, violations of pre-conditions are automatically detected and reported. In addition, abstract visualizations of the objects that are created and manipulated by classes are automatically generated.
In the remainder of this paper, we will summarize the roles that pre-conditions, post-conditions, and abstraction functions can play in specifying the behavior of programs; illustrate how Javiva provides runtime support for such specifications; and survey related work.
Abstraction by Specification
Teaching beginning programmers effective techniques for designing, implementing, and reasoning about abstract data types has long been a concern of educators. In their classic text Abstraction and Specification in Program Development [1], Barbara Liskov and John Guttag address the problem of teaching students to think abstractly. Their text features discussions of abstraction by parameterization and abstraction by specification. This second form of abstraction, in which students are taught to think about functions and classes in terms of their (informally) specified behavior, instead of in terms of their implementations, is particularly powerful. It is also extremely difficult to teach to beginning students. Our goal in developing Javiva is to obtain a tool that will help us teach abstraction by specification. We will discuss the idea of abstraction by specification in this section, and its realization via Javiva in the next.
The key idea behind abstraction by specification is the use of pre-conditions and post-conditions to specify the behavior of functions. Pre-conditions and post-conditions constitute a contract between the designer and the user of a function. A correct function implementation must guarantee that the post-condition will hold upon function exit so long as the pre-condition held upon function entry. Thus, specification by abstraction simplifies the problem of reasoning about the effects of calling a function because only the specification, and not the implementation, must be examined. Similarly, specification by abstraction simplifies the problem of reasoning about the correctness of a function implementation, since the contexts from which the function will be called need not be examined.
For example, consider the specification of the integer-valued
square root function isqrt in Figure 1.
The specification makes it possible to write code that uses isqrt
without seeing its implementation, and it makes it possible to correctly
implement isqrt without seeing the code
that will use it.
| Pre: x >= 0
Post: Returns v: v >= 0, v*v <= x, (v+1)*(v+1) > x. public static int isqrt (int x); |
|
|
Pre-conditions and post-conditions can also be used to
specify the behavior of methods that belong to classes that implement abstract
data types. Consider, for example, Figure 2. It contains the specification
of choose, one of the public methods in
an intset class. It returns an arbitrary element from a non-empty intset.
| Pre: this != emptyset
Post: Returns v: v elementof this public int choose (); |
|
|
Since choose is a method, this is an implicit parameter and can be mentioned in the specification. Notice, however, that both the pre-condition and the post-condition treat this as if it represents a mathematical set of integers. In other words, this is treated abstractly rather than concretely. Otherwise, it would be impossible to specify any method prior to choosing a representation for its class.
A specification of all of the public methods of a class
such as intset makes it possible to write code that uses the class without
having to consult the implementation. However, it does not make
it possible to correctly implement a particular method. This is because
all of the methods of a class must agree on the way in which abstract values
will be represented.
| A(this) = {x | elts[i] = x and 0 ? i < count} |
|
|
An abstraction function is the piece of the documentation of a class that specifies which abstract value any particular representation stands for. For example, suppose that intset objects are represented by an array elts of integers and an integer count. One possible abstraction function is illustrated in Figure 3.
The abstraction function in Figure 3 says that the abstract value for which this stands, A(this), is the set of all integers that are stored in the first count entries of the array elts. This is the kind of representation decision that any implementor of a class must make. Writing down the abstraction function provides extremely good documentation. By specifying each constructor and method, choosing a representation, and deciding on an abstraction function, it is possible to correctly implement each method of a class without having to consult the implementations of any of the other methods.
To illustrate, consider the problem of correctly implementing the choose method given only the abstraction function and the specification of choose. The pre-condition specifies that this will represent a non-empty set; the abstraction function lets us conclude in turn that count will be non-zero. Similarly, the post-condition specifies that the return value must be an element of the set represented by this. The abstraction function shows us that we can accomplish this by choosing any of the first count elements of elts.
Javiva
Abstraction by specification is difficult to teach to students for several reasons. First, there is rarely a payoff for practicing abstraction by specification in the kinds of programs that students write as assignments. Specifications are most useful in connection with large programs that are maintained over a long period of time, not with small programs that are completed and discarded within one week.
Second, and more fundamentally, it is often difficult to come up with a vocabulary with which to specify pre-conditions, post-conditions, and abstraction functions. In the case of isqrt it was natural to use familiar integer notation, and in the case of choose it was natural to use familiar set notation. Imagine, though, trying to specify the behavior of the members of a graph class.
Our goal in designing and implementing Javiva was to eliminate
these two barriers to using abstraction by specification. Students who
wish to exploit the capabilities of Javiva can include pre-conditions and
post-conditions as stylized comments in Java source files. Figure 4 shows
the Javiva-style specification of an isqrt
function.
| /** @pre x >= 0
@post rval >= 0 && rval*rval <= x && (rval+1)*(rval+1) > x **/ public static int isqrt (int x); |
|
|
The pre-conditions and post-conditions are contained inside of comment delimiters. Each condition is a Boolean expression written using standard Java syntax. (The special symbol rval stands for the value that is ultimately returned by the function). When source code is preprocessed by Javiva and then compiled by a Java compiler, the resulting byte code is structured to automatically check pre-conditions and post-conditions at runtime. In the case of Figure 4, the pre-condition will be automatically checked each time isqrt is called, and the post-condition will be automatically checked each time isqrt returns. If a pre-condition or post-condition is violated, the programmer is automatically notified via a pop-up window.
This automatic checking provides a tangible benefit for students who include pre-conditions and post-conditions in their code. In particular, notifications of violations of pre-conditions and post-conditions make it easier to debug programs. This in turn encourages the specification of pre-conditions and post-conditions and reinforces the benefits of abstraction by specification.
Specifying a class method requires an additional twist,
however, since a vocabulary for describing the abstract values that are
represented by the objects of the class must be made available. We address
this issue by providing shadow classes. Part of a shadow integer
set class appears in Figure 5.
| public abstract class ShadowIntSet {
/* Construct an empty set. */
/* Insert n into the set. */
/* Returns the size of the set. */
/* Report whether n belongs to the set. */
} |
|
|
A shadow class is an independent implementation of the abstract data type that the student is implementing. In a course setting, it would typically be provided by the instructor. A student uses a shadow class not to implement his or her own class but as the means of expressing his or her pre-conditions, post-conditions, and abstraction function. In other words, the constructors and methods of the shadow class provide the required vocabulary for creating and manipulating abstract values.
For example, using the shadow class in Figure 5, the Javiva-style
specification of the abstraction function from Figure 3 would be as illustrated
in Figure 6.
| /** @af
ShadowIntSet A () { ShadowIntSet s = new ShadowIntSet(); for (int i = 0; i < count; i++) s.insert(elts[i]); return s; } **/ |
|
|
Thus, an abstraction function in a Java program that is annotated for Javiva appears as a comment. It is a Java method (called A) that converts an arbitrary object (of the student’s class) into the corresponding object of the shadow class. In order to write an abstraction function, a student must first understand the set of abstract values that he or she is trying to provide with his or her class. (This entails understanding the specification of the shadow class provided by the instructor.) The student must then write a function that maps his or her objects to shadow set objects.
When Javiva processes a class that contains an abstraction
function, it instruments the resulting class file so that it contains the
abstraction function as a member function. As a result, the pre-conditions
and post-conditions of the methods of the class can reference the abstraction
function. Consider, for example, the Javiva-style specification of the
choose method in Figure 7.
| /** @pre A().size() > 0
@post A().contains(rval) **/ public int choose (); |
|
|
The pre-condition specifies that the abstract value that corresponds to this must have a size greater than zero, and the post-condition specifies that the returned value must be a member of the abstract value that corresponds to this. At runtime, the pre-condition is checked by first using A() to convert this into a ShadowIntSet and then invoking size(). Similarly, the post-condition is checked by using A() to convert this into a ShadowIntSet and then invoking contains(). The ability to have abstractly-specified pre-conditions and post-conditions that can be automatically checked at runtime is a powerful incentive for students to specify abstraction functions.
The author of a shadow class can, at his or her option,
include a method that produces a visualization of a shadow object. If the
shadow class contains such a method, Javiva will arrange for each of the
objects of the student’s class to contain a method which, when invoked,
will create a visualization of that object. This method works by using
the abstraction function to convert the student object into a shadow object,
and then by using the shadow class’s visualization method to render the
shadow object. The ability to automatically obtain visualizations of objects
is another powerful incentive for students to specify abstraction functions.
A visualization of a student-created binary tree, created by Javiva, appears
in Figure 8.
|
|
|
|
Related Work
The approach to specifying programs promulgated by the Larch [4] project was a major influence on our work. In the Larch approach, pre-conditions and post-conditions are attached to methods. In these conditions, abstract values are described by using algebraic terms created using the Larch shared language. We have adopted Larch’s approach to describing pre-conditions and post-conditions, and have replaced its use of shared language specifications (which are designed to be processed by theorem provers) with Javiva’s use of shadow classes (which are designed to be executed).
iContract [5] is a system for adding checkable assertions to Java programs by using tagged comments, which is very similar to the approach taken by Javiva. These assertions are ultimately incorporated into the byte code and are checked at runtime. The major difference between Javiva and iContract is Javiva’s use of programmer-supplied abstraction functions to make it easier to describe pre-conditions and post-conditions on class methods.
JML [6,7] is also similar to Javiva, and it too was inspired in part by the Larch project. It allows the programmer to attach pre-conditions, post-conditions, and representation invariants to Java programs. Like iContract, however, it does not include support for abstraction functions.
Additionally, of all the tools we looked at to perform verification of code, none of them provided the ability to view the abstract data visually. We felt that this is an important part of the learning process, and was lacking from these tools when used for educational means.
In the example shadow classes that we have constructed to this point, we have used JDSL [3] to render the visualizations. There are a lot of visualization packages besides JDSL, and we view these packages as being complementary to Javiva. In Javiva, all of the code required to produce visualizations is contained in the shadow classes, which are implemented by the instructor using whatever means is most convenient.
Using Javiva
Javiva is a preprocessor that is designed to be used in concert with a standard Java compiler such as Sun Microsystems’ javac. All of the annotations that must be added to a Java source file to exploit Javiva¾ the pre-conditions, post-conditions, and abstraction functions¾ are embedded inside of comments. As a result, if a compiler alone processes an annotated program, the annotations will be ignored.
When Javiva is used, however, the byte code file that results from compiling the class file will be different. Code is added that automatically checks pre-conditions and post-conditions each time an annotated method is called. The abstraction function is added as a public member function. Finally, a method that displays an illustration of the object is added as a public member. All of this is done transparently to the student.
The resulting class file can be used in any Java runtime environment, such as Sun Microsystems’ java. The class files can be used to greatest effect, however, in an interpreted Java development environment such as BlueJ [8], in which it is easy to interactively invoke the visualization method. (For demonstration purposes, we have also created our own extremely simple Java interpreter.)
Javiva can be exploited in CS1 and CS2 classes in several ways. When students are assigned to write stand-alone static functions, they can be given the Javiva-style pre-conditions and post-conditions to use. By incorporating these conditions into their programs, the students will obtain a valuable debugging aid with no overhead on their part.
When students are assigned to implement classes, they can be given the appropriate pre-conditions and post-conditions and be required only to create the abstraction function. (The task of writing abstraction functions can be simplified, if desired, by providing a variety of constructors in the shadow class, one corresponding to each commonly-used type of representation for the student class.) By incorporating the conditions into their programs and creating an abstraction function, the students will obtain both a valuable debugging aid and a valuable visualization aid.
More advanced students who are learning to design their own class interfaces can be asked to create their own pre-conditions, post-conditions, and abstraction functions.
From the viewpoint of the instructor, the major drawback to using Javiva is the need to create shadow classes. We are working to create a library of shadow classes corresponding to the abstract data types that are most commonly used in CS1 and CS2 courses. Naturally, it is our hope that Javiva will become widely used, and that the user community will rapidly enlarge the shadow class library.
Because of space limitations, we have not discussed every aspect of Javiva, and we will close by briefly mentioning three particularly important ones. First, we have included support for specifying and checking the behavior of methods that throw exceptions. Second, we have included support for specifying and checking class representation invariants. Finally, we have included support for referring, in method post-conditions, to both the value that this had when the method was invoked and the method that this has upon method return.
Acknowledgments
This work was supported in part by the National Science Foundation under grant DUE-9972850.
Joe Everton, Paul Scutts, and Herman Vandecastle all contributed to the implementation of Javiva.
References