jContractorRuntime (jContractor API)

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

edu.ucsb.ccs.jcontractor
Class jContractorRuntime

java.lang.Object
  |
  +--edu.ucsb.ccs.jcontractor.jContractorRuntime

public class jContractorRuntime
extends java.lang.Object

This class is used internally by jContractor, and should never be used by others. This class is used to maintain state information while contracts are checked. In particular, it keeps track of which threads are evaluating contracts so that the assertion evaluation rule can be implemented. It also provides a mechanism for storing cloned objects to check OLD references.

One final implementation note: jContractorRuntime is a "magic" class in the jContractor system. Because contract checking code calls the methods of this class, this class cannot have contracts of its own. If it did, then they would need code that called themselves, which wouldn't do at all. So jContractorRuntime must remain contract-less. jContractor will ignore any contracts written for this class.

Assertion Evaluation Rule

The Assertion Evaluation Rule states that when a program is evaluating a contract, no other contracts should be evaluated. What this means is that the contracts of any methods that the first contract calls will not be evaluated.

For example:

   public class MyClass {
     public void foo () {
       return true;
     }

     protected boolean foo_Precondition () {
       return bar();
     }

     public boolean bar () {
       return true;
     }

     protected boolean bar_Precondition () {
       return false;
     }
   }

Calling the foo() method will not result in a contract violation becuase the bar() precondition will not be evaluated while the foo() precondition is under evaluation.

The Assertion Evaluation Rule exists to prevent recursive contract checking, and because it is hard to say what the problem is if an assertion is violated while checking another assertion (which one failed?). The assumption is that if you are calling a method from a contract, you trust that method enough that its contract doesn't need to be checked.

jContractor implements the Assertion Evaluation Rule by locking assertion checking when a thread starts to evaluate an assertion. This is done by calling the lockAssertionCheck() method. No other assertions will be evaluated until the lock has been released by releaseAssertionCheck().

OLD objects

jContactor allows postconditions to refer the state of an object at method entry calling methods on the OLD object, as in "return count == OLD.count() + 1". When execution enters a method whose postcondition refers to OLD, the object is cloned, and the clone is pushed onto a stack held this class. When the postcondition is checked, the cloned object is popped from the stack. All of this is necessary because there may be any number of method calls between method entry and the postcondition check. So OLD may be saved any number of times.

Version:: $Id: jContractorRuntime.java,v 1.4 2002/05/22 06:28:48 parkera Exp $
Author:: Parker Abercrombie

Constructor Summary

jContractorRuntime()


Method Summary

static boolean canCheckAssertion()
          Determine if the current thread can evaluate an assertion.

static void checkpoint()


static void lockAssertionCheck()
          Lock assertion checking for the current thread.

static java.lang.Object popState()
          Recall the last saved state for a thread of execution.

static void pushState(java.lang.Object stateObject)
          Save the state of an object for retrieval later.

static void releaseAssertionCheck()
          Release the assertion checking lock for the current thread.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail