org.jmlspecs.samples.dirobserver
Interface DirObserverKeeper

All Superinterfaces:

Cloneable, JMLType, Serializable

All Known Subinterfaces:

Directory, RODirectory

public interface DirObserverKeeper

extends JMLType

An object that keeps directory observers (i.e., a subject).

Class Specifications

instance public invariant this.listeners != null; public initially !this.in_notifier;

Specifications inherited from class Object

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

Model Field Summary
[instance]  JMLObjectSet	listeners           The set of observers.

 

Ghost Field Summary
[instance]  boolean	in_notifier           Is a notification callback running?

 

Method Summary
boolean	inNotifier()           Is a notifier callback running?
void	register(DirObserver o)           Add a listener to the set of listeners.
void	unregister(DirObserver o)           Take a listener out of the set of listeners.

 

Methods inherited from interface org.jmlspecs.models.JMLType

clone, equals, hashCode

 

Model Field Detail

listeners

public JMLObjectSet listeners

The set of observers.

Specifications: instance

in_notifier

public boolean in_notifier

Is a notification callback running?

Specifications: instance

inNotifier

public boolean inNotifier()

Is a notifier callback running?

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result == this.in_notifier;

register

public void register(DirObserver o)

Add a listener to the set of listeners.

Specifications:

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

unregister

public void unregister(DirObserver o)

Take a listener out of the set of listeners.

Specifications:

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