org.jmlspecs.samples.dirobserver
Interface RODirectory

All Superinterfaces:

Cloneable, DirObserverKeeper, JMLType, Serializable

All Known Subinterfaces:

Directory

public interface RODirectory

extends DirObserverKeeper

Read-only directories.

Class Specifications

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 class Object

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

Specifications inherited from interface DirObserverKeeper

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

Model Field Summary
[instance]  JMLValueToObjectMap	entries           This models the directory's mapping from strings to files.

 

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
boolean	equals(nullable Object oth)           Test whether this object's value is equal to the given argument.
File	thisFile(String n)           Return the file with the given name in this directory.

 

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

inNotifier, register, unregister

 

Methods inherited from interface org.jmlspecs.models.JMLType

clone, hashCode

 

Model Field Detail

entries

public JMLValueToObjectMap entries

This models the directory's mapping from strings to files.

Specifications: instance

thisFile

public File thisFile(String n)

Return the file with the given name in this directory.

Specifications:

public normal_behavior
requires n != null&&!n.equals("");

{|

requires this.entries.isDefinedAt(new org.jmlspecs.models.JMLString(n));
assignable \nothing;
ensures \result .equals((org.jmlspecs.samples.dirobserver.File)this.entries.apply(new org.jmlspecs.models.JMLString(n)));

also

requires !this.entries.isDefinedAt(new org.jmlspecs.models.JMLString(n));
assignable \nothing;
ensures \result == null;

|}

equals

public boolean equals(nullable Object oth)

Description copied from interface: JMLType

Test whether this object's value is equal to the given argument.

Specified by:

equals in interface JMLType

Overrides:

equals in class Object

Specifications: pure

     also

public normal_behavior

{|

requires !(oth instanceof org.jmlspecs.samples.dirobserver.RODirectory);
ensures \result == false;

also

requires oth instanceof org.jmlspecs.samples.dirobserver.RODirectory;
ensures \result == (this.entries.equals(((org.jmlspecs.samples.dirobserver.RODirectory)oth).entries)&&this.listeners.equals(((org.jmlspecs.samples.dirobserver.RODirectory)oth).listeners));

|}

Specifications inherited from overridden method equals(Object obj) in class Object:
       pure

public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);

     also

public normal_behavior
requires this == obj;
ensures \result ;

     also

public code normal_behavior
requires obj != null;
ensures \result <==> this == obj;

     also

diverges false;
ensures obj == null ==> !\result ;

Specifications inherited from overridden method equals(Object ob2) in interface JMLType:
       pure

     also

public normal_behavior
ensures \result ==> ob2 != null&&(* ob2 is not distinguishable from this, except by using mutation or == *);

    implies_that

public normal_behavior

{|

requires ob2 != null&&ob2 instanceof org.jmlspecs.models.JMLType;
ensures ((org.jmlspecs.models.JMLType)ob2).equals(this) == \result ;

also

requires ob2 == this;
ensures \result <==> true;

|}