org.jutil.structure
Class DoubleBinding

java.lang.Object
  |
  +--org.jutil.structure.DoubleBinding

public class DoubleBinding

extends java.lang.Object

DEPRECATEDA class of "components" for implementing a double binding.

This is actually a lightweight version of the APSet-APElement combination of the Beedra framework of Jan Dockx.

The classes that are linked together should still be in the same package, but are easier to implement using DoubleBinding. A "native" binding is more efficient, but an optimizer could do the transformation in order to get both the programming and the efficiency benefits.

This class is typically used in the following way:

 public class A {
   public A() {
     $b= new DoubleBinding(this);
   }
 
   public B getB() {
     return (B)$b.getOtherEnd();
   }
 
   public void setB(B b) {
     if (b != null) {
       $b.setOtherBinding(b.getALink());
     }
     else {
       $b.setOtherBinding(null);
     }
   }
 
   private DoubleBinding $b;
   private String $name;
 }
 
 public class B {
 
   public B() {
     $a = new DoubleBinding(this);
   }
 
   public A getA() {
     return (A)$a.getOtherEnd();
   }
 
   DoubleBinding getALink() {
     return $a;
   }
   private String $name;
 }

Class Specifications

public invariant getObject() != null; public invariant getOtherBinding() != null ==> getOtherBinding().getOtherBinding() == this;

Field Summary
static java.lang.String	CVS_REVISION           Deprecated.

 

Constructor Summary

DoubleBinding(java.lang.Object object)           Deprecated. Initialize a new unconnected DoubleBinding.

DoubleBinding(DoubleBinding otherBinding, java.lang.Object object)           Deprecated. Initialize a new double binding connected to the given other DoubleBinding.

 

Method Summary
java.lang.Object	getObject()           Deprecated. Return the object at this side of the double binding.
DoubleBinding	getOtherBinding()           Deprecated. Return the DoubleBinding object this one is connected to.
java.lang.Object	getOtherEnd()           Deprecated. Return the Object at the other end of this double binding.
boolean	isConnected()           Deprecated. Check whether or not this DoubleBinding is connected to another.
void	setOtherBinding(DoubleBinding otherBinding)           Deprecated. Set the other end of this binding

 

Methods inherited from class java.lang.Object

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

 

Field Detail

CVS_REVISION

public static final java.lang.String CVS_REVISION

Deprecated. 

DoubleBinding

public DoubleBinding(java.lang.Object object)

Deprecated. 

Initialize a new unconnected DoubleBinding.

Parameters:

object - The object on this side of the double binding

Specifications:

public behavior
requires object != null;
ensures getOtherBinding() == null;
ensures getObject() == object;

DoubleBinding

public DoubleBinding(DoubleBinding otherBinding,
                     java.lang.Object object)

Deprecated. 

Initialize a new double binding connected to the given other DoubleBinding.

Parameters:

other - The DoubleBinding object to connect to.

object - The object on this side of the double binding

Specifications:

public behavior
requires object != null;
ensures getOtherBinding() == otherBinding;
ensures otherBinding != null ==> otherBinding.getOtherBinding() == this;
ensures (otherBinding != null)&&\old(otherBinding.getOtherBinding()) != null ==> \old(otherBinding.getOtherBinding()).getOtherBinding() == null;
ensures getObject() == object;

getObject

public java.lang.Object getObject()

Deprecated. 

Return the object at this side of the double binding.

isConnected

public boolean isConnected()

Deprecated. 

Check whether or not this DoubleBinding is connected to another.

getOtherEnd

public java.lang.Object getOtherEnd()

Deprecated. 

Return the Object at the other end of this double binding.

Specifications:

public behavior
ensures getOtherBinding() == null ==> \result == null;
ensures getOtherBinding() != null ==> \result == getOtherBinding().getObject();

getOtherBinding

public DoubleBinding getOtherBinding()

Deprecated. 

Return the DoubleBinding object this one is connected to.

setOtherBinding

public void setOtherBinding(DoubleBinding otherBinding)

Deprecated. 

Set the other end of this binding

Parameters:

otherBinding - The new DoubleBinding object that will be connected to this.

Specifications:

public behavior
ensures getOtherBinding() == otherBinding;
ensures \old(getOtherBinding()) != null&&\old(getOtherBinding()) != otherBinding ==> \old(getOtherBinding()).getOtherBinding() == null;
ensures otherBinding != null ==> otherBinding.getOtherBinding() == this;
ensures otherBinding != null&&\old(otherBinding.getOtherBinding()) != null&&\old(otherBinding.getOtherBinding()) != this ==> \old(otherBinding.getOtherBinding()).getOtherBinding() == null;