org.jutil.structure
Class DoubleBinding

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

public class DoubleBinding

extends java.lang.Object

A 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;
 }

Version:

$Revision: 1.5 $

Author:

Marko van Dooren

Field Summary

static java.lang.String

CVS_REVISION

Constructor Summary

DoubleBinding(DoubleBinding other, java.lang.Object object)
public behavior

pre object != null;

post getOtherBinding() == otherBinding;
post otherBinding != null ==> otherBinding.getOtherBinding == this;
// If was connected before to another object, that other object will
// be disconnected.
post (otherBinding != null) && \old(otherBinding.getOtherBinding()) != null ==>
\old(otherBinding.getOtherBinding()).getOtherBinding() == null;
post getObject() == object;
Initialize a new double binding connected to the given other DoubleBinding.

DoubleBinding(java.lang.Object object)
public invariant getObject() != null;
public invariant getOtherBinding() != null =>
getOtherBinding().getOtherBinding() == this;

public behavior

pre object != null;

post getOtherBinding() == null;
post getObject() == object;
Initialize a new unconnected DoubleBinding.

Method Summary

java.lang.Object	getObject() Return the object at this side of the double binding.
DoubleBinding	getOtherBinding() Return the DoubleBinding object this one is connected to.
java.lang.Object	getOtherEnd() public behavior post getOtherBinding() == null => \result == null; post getOtherBinding() != null => \result == getOtherBinding().getObject(); Return the Object at the other end of this double binding.
boolean	isConnected() Check whether or not this DoubleBinding is connected to another.
void	setOtherBinding(DoubleBinding otherBinding) public behavior post getOtherBinding() == otherBinding; // If this DoubleBinding was connected before, and will now be // connected to another DoubleBinding, the DoubleBinding it was // connected to will be disconnected. post \old(getOtherBinding()) != null && \old(getOtherBinding()) != otherBinding => \old(getOtherBinding()).getOtherBinding() == null; post otherBinding != null ==> otherBinding.getOtherBinding() == this; // If was connected before to another object, that other object will // be disconnected. post otherBinding != null && \old(otherBinding.getOtherBinding()) != null && \old(otherBinding.getOtherBinding()) != this ==> \old(otherBinding.getOtherBinding()).getOtherBinding() == null; 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

Constructor Detail

DoubleBinding

public DoubleBinding(java.lang.Object object)

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

public behavior

pre object != null;

post getOtherBinding() == null;
post getObject() == object;
Initialize a new unconnected DoubleBinding.

Parameters:

object - The object on this side of the double binding

DoubleBinding

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

public behavior

pre object != null;

post getOtherBinding() == otherBinding;
post otherBinding != null ==> otherBinding.getOtherBinding == this;
// If was connected before to another object, that other object will
// be disconnected.
post (otherBinding != null) && \old(otherBinding.getOtherBinding()) != null ==>
\old(otherBinding.getOtherBinding()).getOtherBinding() == null;
post getObject() == object;
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

Method Detail

getObject

public java.lang.Object getObject()

Return the object at this side of the double binding.

isConnected

public boolean isConnected()

Check whether or not this DoubleBinding is connected to another.

getOtherEnd

public java.lang.Object getOtherEnd()

public behavior

post getOtherBinding() == null => \result == null;
post getOtherBinding() != null => \result == getOtherBinding().getObject();
Return the Object at the other end of this double binding.

getOtherBinding

public DoubleBinding getOtherBinding()

Return the DoubleBinding object this one is connected to.

setOtherBinding

public void setOtherBinding(DoubleBinding otherBinding)

public behavior

post getOtherBinding() == otherBinding;
// If this DoubleBinding was connected before, and will now be
// connected to another DoubleBinding, the DoubleBinding it was
// connected to will be disconnected.
post \old(getOtherBinding()) != null && \old(getOtherBinding()) != otherBinding =>
\old(getOtherBinding()).getOtherBinding() == null;
post otherBinding != null ==> otherBinding.getOtherBinding() == this;
// If was connected before to another object, that other object will
// be disconnected.
post otherBinding != null &&
\old(otherBinding.getOtherBinding()) != null &&
\old(otherBinding.getOtherBinding()) != this ==>
\old(otherBinding.getOtherBinding()).getOtherBinding() == null;
Set the other end of this binding

Parameters:

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