Programming By Contract Thin Tool

Concept programming is designed mostly with custom concepts in mind. However, some concepts are so successful that they cause a deep change in the way we program: program structures led for structured programming, objects led to object-oriented programming. Such a change is called a paradigm shift. Some other techniques don't become quite so mainstream, but they become prominent at least in a niche: programming by contract with Eiffel, tasking with Ada, logic programming with Prolog.

Concept programming let you implement and then use such new paradigm, whether they are supported by your favorite language or not, whether they are mainstream or not. As an illustration, the assert thin tool shows how a modest plug-in can extend a language such as Java and give it "programming by contract" capabilities similar to those in Eiffel. The plug-in implements not only simple assertions (like those implemented using macros in C), but also more complicated forms of class invariants that would be extremely tedious to check manually.

Assertions Syntax in Java code

The assert plug-in extends the Java language as follows:

• Assertions are checked using the assert pseudo-function.
• Member preconditions and postconditions are specified in two special member functions called precondonditions and postconditions respectively.
• Class invariants are specified in the invariants special member function.

Below is an example of Stack class implementation that contains such assertions:

class Stack
{  
   public Stack()
   {  
      objects = new Object[MAX];
      top = 0;
   }
   public void Push(Object o)
   {  
      objects[top] = o;
      top++;
   }
   public Object Pop()
   {  
      top--;
      return  objects[top];
   }
   public int Size()
   {  
      return  top;
   }
   
   private int Remaining()
   {  
      assert (false);
      return  MAX - top;
   }
   
   private Object[] objects;
   private int top;
   private static final int MAX = 10;
   
   preconditions()
   {  
      Push:
      top < MAX;
      Pop:
      top > 0;
   }
   
   postconditions()
   {  
      Push:
      top > 0;
   }
   
   invariants()
   {  
      top >= 0;
      top <= MAX;
   }
}

Checking assertions

The plug-in is invoked from Moka using the +assert:on option to enable assertion checking:

% moka tests/asserts.small.java +assert:on -out

When assertions are enabled, the plug-in inserts all the necessary tests, and invokes a method assertion_failed if any of the tests fail. The generated code, whch would be quite tedious to generate manually, looks like the following:

class Stack
{  
   public Stack()
   {  
      try
      {  
         if(!(top >= 0))
            assertion_failed ("invariant #1 on entry in Stack", 0);
         if(!(top <= MAX))
            assertion_failed ("invariant #2 on entry in Stack", 1);
         objects = new Object[MAX];
         top = 0;
      }
      finally
      {  
         if(!(top >= 0))
            assertion_failed ("invariant #1 on exit from Stack", 2);
         if(!(top <= MAX))
            assertion_failed ("invariant #2 on exit from Stack", 3);
      }
   }
   public void Push(Object o)
   {  
      try
      {  
         if(!(top >= 0))
            assertion_failed ("invariant #1 on entry in Push", 5);
         if(!(top <= MAX))
            assertion_failed ("invariant #2 on entry in Push", 6);
         if(!(top < MAX))
            assertion_failed ("Push precondition #1", 4);
         objects[top] = o;
         top++;
      }
      finally
      {  
         if(!(top > 0))
            assertion_failed ("Push postcondition #1", 7);
         if(!(top >= 0))
            assertion_failed ("invariant #1 on exit from Push", 8);
         if(!(top <= MAX))
            assertion_failed ("invariant #2 on exit from Push", 9);
      }
   }
   public Object Pop()
   {  
      try
      {  
         if(!(top >= 0))
            assertion_failed ("invariant #1 on entry in Pop", 11);
         if(!(top <= MAX))
            assertion_failed ("invariant #2 on entry in Pop", 12);
         if(!(top > 0))
            assertion_failed ("Pop precondition #1", 10);
         top--;
         return  objects[top];
      }
      finally
      {  
         if(!(top >= 0))
            assertion_failed ("invariant #1 on exit from Pop", 13);
         if(!(top <= MAX))
            assertion_failed ("invariant #2 on exit from Pop", 14);
      }
   }
   public int Size()
   {  
      try
      {  
         if(!(top >= 0))
            assertion_failed ("invariant #1 on entry in Size", 15);
         if(!(top <= MAX))
            assertion_failed ("invariant #2 on entry in Size", 16);
         return  top;
      }
      finally
      {  
         if(!(top >= 0))
            assertion_failed ("invariant #1 on exit from Size", 17);
         if(!(top <= MAX))
            assertion_failed ("invariant #2 on exit from Size", 18);
      }
   }
   
   private int Remaining()
   {  
      if(!false)
         assertion_failed ("Remaining assert #19", 19);
      return  MAX - top;
   }
   
   private Object[] objects;
   private int top;
   private static final int MAX = 10;
}

Generating Production Code

For production code, the assertion checking can be disabled, using the +assert:off option to disable assertion checking:

% moka tests/asserts.small.java +assert:off -out

In this case, the previous Stack class is simplified, and all assertion-related extensions are removed:

class Stack
{  
   public Stack()
   {  
      objects = new Object[MAX];
      top = 0;
   }
   public void Push(Object o)
   {  
      objects[top] = o;
      top++;
   }
   public Object Pop()
   {  
      top--;
      return  objects[top];
   }
   public int Size()
   {  
      return  top;
   }
   
   private int Remaining()
   {  
      /* Nop */;
      return  MAX - top;
   }
   
   private Object[] objects;
   private int top;
   private static final int MAX = 10;
}