org.jmlspecs.samples.dirobserver
Interface DirObserver

public interface DirObserver

Observers (i.e. listeners) in the directory system.

Class Specifications

Specifications inherited from class Object

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

Model Field Summary
[instance]  JMLDataGroup	obsState           The state of this observer.

 

Method Summary
void	addNotification(Directory o, String n)           Receive a notification that a given name is being added to the given directory.
void	removeNotification(Directory o, String n)           Receive a notification that a given name is being removed from the given directory.

 

Model Field Detail

obsState

public JMLDataGroup obsState

The state of this observer.

Specifications: instance

addNotification

public void addNotification(Directory o,
                            String n)

Receive a notification that a given name is being added to the given directory.

Specifications:

public normal_behavior
requires o != null&&o.in_notifier&&n != null&&!n.equals("");
assignable obsState;
ensures o.equals(\old(o));

removeNotification

public void removeNotification(Directory o,
                               String n)

Receive a notification that a given name is being removed from the given directory.

Specifications:

public normal_behavior
requires o != null&&o.in_notifier&&n != null&&!n.equals("");
assignable obsState;
ensures o.equals(\old(o));