Implementing Assertions for Java
by Jeffery E. Payne, Michael A. Schatz, Matthew Schmid

Example 1: 

 . . .
Coordinate x, old_x ; 
x = new Location() ;
x.setValue(5);
old_x = x ;
x.setValue(10) ;
 . . .


Listing One
public class math
{ 
private static int double_it(int x)
  {
    /*+ PRE_CONDITION( $RETURN = 2 * $OLD(x), "didn't double correclty"); +*/
    x *= 3;
    return x;
  }
public static int sqrt(int x)
  {
    /*+ PRE_CONDITION(x >= 0, "Can't take the sqrt of a negative number"); +*/
    int i;
    for (i=0;i*i <= x; i++)
      {
      }
    return i-1;
  }
public static void switcheroo(char c)
  {
    switch ( c )
      {
      case 'm' :
      case 'M' :  System.out.print("Male");  break;
      case 'f' :
      case 'F' :  System.out.print("Female");  break;
      default :  /*+ ASSERT(false, "Not a valid gender!");  +*/  break;
      }
  }
public static void main(String argv[])
  {
    /*  These all work:  */
    System.out.println("2 * 0 = " + double_it(0));
    System.out.println("sqrt(9) = " + sqrt(9));
    switcheroo('m');
    System.out.print(" ");
    switcheroo('f');
    System.out.println();
    /*  These all fail */
    System.out.println("2 * 3 = " + double_it(3));
    System.out.println("sqrt(-9) = " + sqrt(-9));
    switcheroo('q');
  }
} 
}

Listing Two
import java.io.*;
public class Assert
{
private static String getStackTrace()
  {
    Throwable t = new Throwable();
    ByteArrayOutputStream os = new ByteArrayOutputStream();
    PrintStream ps = new PrintStream(os);
    t.printStackTrace(ps);
    return os.toString();
  }
public static void PreCondition(boolean condition, String message)
  {
    if (!condition)
      {
        System.out.println("Precondition [" + message + "] fired at:");
        System.out.println(getStackTrace());
        System.exit(1);
      }
  }  
public static void Assert(boolean condition, String message)
  {
    if (!condition)
      {
        System.out.println("Assert [" + message + "] fired at:");
        System.out.println(getStackTrace());
        System.exit(1);
      }
  }  
public static void PostCondition(boolean condition, String message)
  {
    if (!condition)
      {
        System.out.println("Postcondition [" + message + "] fired at:");
        System.out.println(getStackTrace());
        System.exit(1);
      }
  }  
public static void main(String argv[])
  {
    PreCondition(true, "this is a test");
    PreCondition(false, "this is another test");
  }
}


Listing Three
public class math
{ 
private static int double_it(int x)
  {
    int ret = x*3;
    Assert.PostCondition(ret == 2*x, "didn't double correctly"); 
    return ret;
  }
public static int sqrt(int x)
  {
    Assert.PreCondition(x >= 0, "Can't take the sqrt of a negative number"); 
    int i;
    for (i=0;i*i <= x; i++)
      {
      }
    return i-1;
  }
public static void switcheroo(char c)
  {
    switch ( c )
      {
      case 'm' :
      case 'M' :  System.out.print("Male");  break;
      case 'f' :
      case 'F' :  System.out.print("Female");  break;
      default :  Assert.Assert(false, "Not a valid gender!"); break;
      }
  }
public static void main(String argv[])
  {
    /*  These all work:  */
    System.out.println("2 * 0 = " + double_it(0));
    System.out.println("sqrt(9) = " + sqrt(9));
    switcheroo('m');
    System.out.print(" ");
    switcheroo('f');
    System.out.println();
    /*  These all fail */
    System.out.println("2 * 3 = " + double_it(3));
    System.out.println("sqrt(-9) = " + sqrt(-9));
    switcheroo('q');
  }




3