The Jass Page


Refinement - Overview

[English] printer friendly version

1 Notion and motivation

With 'design by contract' a formal specification of a class can be expressed and checked at runtime. Finding a simple and abstract specification and cover all details of the implementation are contrary goals. A possible solution is to refine an abstract class step by step. Each refinement in this process reduces non determinism and makes the class more applicable. Technically such a refinement step may be done through inheritance.

But what is the difference between refinement and inheritance? Refinement in Jass is a special form of inheritance with certain constraints introduced in the second section.

Java has certain constrains for inheritance. For example if a subclass overrides a method of the superclass the new defined method

  1. must be as accessible as the old method,
  2. must have the same return type and
  3. must declare the same formal parameters.

Methods in the superclass are called abstract (This does not mean methods with abstract modifier!), in the subclass they are called concrete. The constrains guaranties that a subclass can appear where the superclass is expected. This property is very typically for object oriented programming. An assignment of the form

 T x = E;

is for example type-correct if the type of the expression E is a subclass of the type T.

For design by contract, the constrains given through the Java language specification for inheritance are not enough. A subclass must maintain the contract (or the specification) of the superclass. The next part describes how this can be guarantied.

2 Refinement

A subclass refines his superclass if for all overwritten methods hold:

  1. If the abstract method is applicable the concrete one can be invoked too.
  2. The concrete method is more deterministic then the abstract one.
  3. Whenever the invariant of the subclass holds the invariant of the superclass must be valid too.

With other words: The precondition of the concrete method must be weaker than the precondition of the abstract method. This means a state that satisfies the abstract precondition must satisfies the concrete precondition too. On the other hand the postcondition of the concrete method must be stronger than the postcondition of the abstract method. This means (if the abstract method is applicable) the concrete method will only return in a state that satisfies the abstract postcondition too.

Refinement does not only cover pre- and postconditions. The invariant must be considered too. The subclass should own a no surprise requirement (Wing). A state that holds for the invariant of the subclass must hold for the invariant of the superclass too.

A subclass that is a refinement of his superclass can appear where the superclass is expected. The subclass maintains the contract of the superclass and perhaps makes it better.

Let us consider an example. The following (abstract) method adds an element in a limited buffer. The method can be invoked if the buffer is not full and the parameter o is not the null reference. After execution the counter in has been incremented.

public void addElement (Object o) {
  /** require !isFull(); o != null; **/
  buffer[in % buffer.length] = o;
  /** ensure changeonly{in,buffer}; == in - 1; **/

The concrete version of the buffer perhaps deals with null references. If the parameter is null the method generates a default element and adds it.

public void addElement (Object o) {
  /** require !isFull(); **/
  if (o==null) 
    buffer[in % buffer.length] = new Default();
    buffer[in % buffer.length] = o;
  /** ensure changeonly{in,buffer}; 
    == in - 1; 
             o!=null ? contains(o) : true; 

The concrete precondition is weaker than the abstract one. With other words: The abstract precondition implies the concrete precondition. The new postcondition is stronger than the old one. It guaranties that the element that should be inserted is contained after the execution of the method. Of course we have expected this, but it was not formally specified in the first example.

A subclass inherits non private fields from the superclass. These fields can be overwritten through the subclass (Of course this is not a good technique!). Private fields are not inherited. In this context a problem arises: The subclass can have a different state space than the superclass. If we want to proof if a precondition of the subclass is weaker than a precondition of the superclass we need the values of all involved fields. But given a subclass we do not know the values of the superclass in generally (Remember the private fields.).

The solution can be found in refinement theory. We can use an abstraction function that maps a concrete state of the subclass on a abstract state of the superclass. This is also know as backwards simulation.

The next part explains how refinement and the abstraction function is realized in Jass.

3 Refinement in Jass

An important design decision was the question if the programmer must use refinement if he subclasses a class or if he can drop this concept. We have implemented the second possibility. The programmer can use refinement but he must not. Refinement requires a theoretically background and the search of an abstraction function is not easy. But Jass should be easy to use and improve correctness with minimal exertion.

If the programmer wants a subclassing to be a refinement he must implement the interface jass.runtime.refinement (Which contains no methods.). This signals the precompiler to add extra refinement checks in the resulting Java code. The checks for the pre- and postconditions and invariant are done by runtime. For example the precompiler adds a check of the form

 pre_a && !pre_c

at the beginning of the method. This is equivalent to: The abstract precondition does not imply the concrete precondition.

If this check is a success (This is not a success for the programmer!) a jass.runtime.RefinementException is thrown. This is a new type of an error in design by contract. Until this point we have had a server fault if the postcondition does not hold and a client fault if the precondition does not hold. The refinement fault covers the relationship between subclass and superclass. It is a design fault.

The programmer must implement the abstraction function in form of a method jassGetSuperState which must return a reference of the type of the superclass. The returned instance must be in an abstract state that is mapped from the concrete state through the abstraction function.

For example if the abstraction function is the identity the method will look like this:

private theAbstractClass jassGetSuperState() {
  return (theAbstractClass)this;

The abstraction function is the identity if all fields are visible in the subclass and if they maintain their semantics.

A more complex example is the UnlimitedBuffer in the examples package of the Jass precompiler. The UnlimitedBuffer is a subclass of the Buffer class that can contain an unlimited amount (theoretically) of elements. The data-structure of the subclass is not longer an array. The buffer is implemented through a java.util.Vector. You can view the complete code here.

private Buffer jassGetSuperState() {
    Buffer b = new Buffer(v.size()+1); = v.size();
    b.out = 0;
    for (int i = 0; i < b.buffer.length-1; i++)
        b.buffer[i] = v.elementAt(i);
    return b;

This method constructs a abstract buffer that represents the current state of the new one. This would be a buffer that can pick up one more element at every moment (It is unlimited somehow.).

Remember if you want an inheritance to be an refinement:

  1. Add jass.runtime.Refinement to the interfaces of the class.
  2. Implement the function jassGetSuperState. Perhaps you can use the identity.

Jass then generates code for refinement checks like code for the other assertions.

4 Refinement in Eiffel

If a programmer uses inheritance in Eiffel he must add the precondition of the superclass to the precondition of the subclass with a logical OR. The postcondition of the superclass must be added to the postcondition of the subclass with a logical AND. Of course this will weaken the precondition and strengthen the postcondition automatically. An abstraction function can not be used, thus the state spaces are always identically.