org.jmlspecs.samples.dirobserver
Interface Directory

All Superinterfaces:

Cloneable, DirObserverKeeper, JMLType, RODirectory, Serializable

public interface Directory

extends RODirectory

Directories that can be both read and written.

Class Specifications

Specifications inherited from class Object

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

Specifications inherited from interface RODirectory

instance public invariant this.entries != null&&( \forall org.jmlspecs.models.JMLType o; this.entries.isDefinedAt(o); o instanceof org.jmlspecs.models.JMLString); instance public invariant ( \forall org.jmlspecs.models.JMLString s; this.entries.isDefinedAt(s); this.entries.apply(s) instanceof org.jmlspecs.samples.dirobserver.File); public initially this.entries != null&&this.entries.equals(new org.jmlspecs.models.JMLValueToObjectMap());

Specifications inherited from interface DirObserverKeeper

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

Model Field Summary

 

Model fields inherited from interface org.jmlspecs.samples.dirobserver.RODirectory

entries

 

Model fields inherited from interface org.jmlspecs.samples.dirobserver.DirObserverKeeper

listeners

 

Ghost Field Summary

 

Ghost fields inherited from interface org.jmlspecs.samples.dirobserver.DirObserverKeeper

in_notifier

 

Method Summary
void	addEntry(String n, File f)
void	removeEntry(String n)

 

Methods inherited from interface org.jmlspecs.samples.dirobserver.RODirectory

equals, thisFile

 

Methods inherited from interface org.jmlspecs.samples.dirobserver.DirObserverKeeper

inNotifier, register, unregister

 

Methods inherited from interface org.jmlspecs.models.JMLType

clone, hashCode

 

Method Detail

addEntry

public void addEntry(String n,
                     File f)

Specifications:

public model_program { ... }

removeEntry

public void removeEntry(String n)

Specifications:

public model_program { ... }