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
Model fields inherited from interface org.jmlspecs.samples.dirobserver.DirObserverKeeper
Ghost Field Summary
Ghost fields inherited from interface org.jmlspecs.samples.dirobserver.DirObserverKeeper
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


public void addEntry(String n,
                     File f)
public model_program { ... }


public void removeEntry(String n)
public model_program { ... }


JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.