jContractorRuntime

Overview

Package

Class

Use

Deprecated

Index

Home >> All >> edu >> ucsb >> ccs >> [ jcontractor overview ]

PREV CLASS NEXT CLASS

SUMMARY:

JAVADOC |

Sourc code of edu.ucsb.ccs.jcontractor.jContractorRuntime

SOURCE |

Download edu.ucsb.ccs.jcontractor.jContractorRuntime

DOWNLOAD | 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 $

Field Summary

protected static java.util.Hashtable savedStates
          A hashtable of Stacks, each of which cooresponds to the execution of a Thread.

protected static java.util.HashSet threadsCheckingContracts
          Set of Threads that are checking assertion.

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

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

Field Detail

threadsCheckingContracts

protected static java.util.HashSet threadsCheckingContracts

Set of Threads that are checking assertion. Further contracts should not be checked on these threads.

savedStates

protected static java.util.Hashtable savedStates

A hashtable of Stacks, each of which cooresponds to the execution of a Thread. As the thread executes, it will need to save the state of objects to check OLD conditions in the postcondition. Of course, between saving state and evaluating the postcondition there may be any number of calls to other methods that need to save state, or even recursive calls requiring multiple saves. In order to keep all of these saved objects in order, they are pushed onto a stack held in this table.

See Also:: pushState(Object) 55 , popState() 55

Constructor Detail