java.util
Class Observable

java.lang.Object
  java.util.Observable

public class Observable

extends Object

JML's specification of the java.util.Observable.

Version:

$Revision: 1.10 $

Author:

Gary T. Leavens

Class Specifications

public invariant ( \forall java.lang.Object o; this.observers.has(o); o instanceof java.util.Observer);

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary
boolean	_changed
JMLEqualsSet	observers

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Constructor Summary

Observable()

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	addObserver(Observer o)
protected  void	clearChanged()
int	countObservers()
void	deleteObserver(Observer o)
void	deleteObservers()
boolean	hasChanged()
void	notifyObservers()
void	notifyObservers(Object arg)
protected  void	setChanged()

 

Methods inherited from class java.lang.Object

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

 

Model Field Detail

observers

public JMLEqualsSet observers

Specifications: non_null

_changed

public boolean _changed

Observable

public Observable()

Specifications:

public normal_behavior
assignable observers, _changed;
ensures this.observers.isEmpty()&&!this._changed;

addObserver

public void addObserver(Observer o)

Specifications:

public normal_behavior
requires o != null;
assignable observers;
ensures this.observers.equals(\old(this.observers.insert(o)));

deleteObserver

public void deleteObserver(Observer o)

Specifications:

public normal_behavior
requires o != null;
assignable observers;
ensures this.observers.equals(\old(this.observers.remove(o)));

notifyObservers

public void notifyObservers()

Specifications:

public normal_behavior
requires !this._changed;
assignable \nothing;

     also

public model_program { ... }

notifyObservers

public void notifyObservers(Object arg)

Specifications:

public normal_behavior
requires !this._changed;
assignable \nothing;

     also

public model_program { ... }

deleteObservers

public void deleteObservers()

Specifications:

public normal_behavior
assignable observers;
ensures this.observers.isEmpty();

setChanged

protected void setChanged()

Specifications:

protected normal_behavior
assignable _changed;
ensures this._changed;

clearChanged

protected void clearChanged()

Specifications:

protected normal_behavior
assignable _changed;
ensures !this._changed;

hasChanged

public boolean hasChanged()

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result <==> this._changed;

countObservers

public int countObservers()

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result == this.observers.int_size();