IBDLObject Class

The IBDL IBDLObject class is a superclass of all validation classes (see below) that provides the implementation of the IBDL operators ``#'' and param which are common to the translation of any IBDL specification. The implementation of these methods is fairly straightforward and follows the informal semantics described in section 3.

It includes the record method that records a message in the history only if the message terminated normally.

class IBDLAccount extends IBDLObject
                  implements Account
{
   /* The object under test.  */
   final Account accountObj;

   /* The constructor of this class.  */
   IBDLAccount(int acNum, int initialBalance)
   {
      MessageSend ms =
        new AccountMsg(acNum, initialBalance);
      record(ms); ms.Validate();
   }
   /* Class that represents a call to the
      ClearCheck method.  */
   class ClearCheckMsg extends MessageSend {
      ClearCheckMsg(int amount)
          throws InvalidAmount, NotEnoughFunds
      {
         super("ClearCheck", 1);
         AddParam(0, amount);
         prev = lastMessage;
         lastMessage = this;

         try { /* Call the method.  */
            StoreReturnValue(
               accountObj.ClearCheck(amount));
         } catch (InvalidAmount t1) {
            StoreException(t1);
         }
         catch (NotEnoughFunds t2) {
            StoreException(t2);
         }
         catch (Throwable t) {
            StoreException(t);
         }
      }

      public boolean IsNormal() {
         if ((exception instanceof
                           InvalidAmount ||
              exception instanceof
                           NotEnoughFunds)) {
            if (exception instanceof
                           InvalidAmount) {
               if (((Integer)GetParam(0)).
                               intValue() < 0)
                  return false;
               throw new Error("Test failed."+
                " The definition of abnormal" +
                 " is not satisfied");
            }
            return false;
         }
         return true;
      }

      public boolean Enabled(String name,
                             Object[] params)
      {
         if (IsNormal()) {
            switch(messageNames.indexOf(name))
            {
               case 2 :  // ClearCheck
                  int i = ((Integer)params[0]).
                                    intValue();
                  Object[] newParams = {
                      new Integer(i +
                          ((Integer)GetParam(0)).
                                  intValue()), };
                  if (!prev.Enabled(name,
                                  newParams))
                     return false;
                  break;
            }
         }
         return prev.Enabled(name, params);
      }
   }
   /* Method to call the ClearCheck method
      on the Account object.  */
   public boolean ClearCheck(int amount)
      throws InvalidAmount, NotEnoughFunds
   {
      MessageSend ms =
               new ClearCheckMsg(amount);
      record(ms); ms.Validate();
      if (ms.exceptionThrown) {
         throw ms.exception;
      }
      return ((Boolean)ms.retVal).
                       booleanValue();
   }
   /* Code for Deposit and the constructor
      will be similar */
}