JML

org.jmlspecs.lang
Interface JMLSetType


public interface JMLSetType

Common protocol for the JML set model types. This is put in org.jmlspecs.lang because the language creates sets using set comprehensions. It should also be useful for the runtime assertion checker and other tools, to know what it can count on from the JML set types.

Version:
$Revision: 1.2 $
Author:
Gary T. Leavens
See Also:
JMLCollection, JMLEqualsSet, JMLValueSet, JMLObjectSet

Class Specifications

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Method Summary
 Object choose()
          Return an arbitrary element of this.
 boolean equals(nullable Object s2)
           
 boolean has(Object elem)
          Tell whether the argument is equal to one of the elements in this collection, using the notion of element equality appropriate for the collection.
 JMLSetType insert(Object elem)
          Returns a new set that contains all the elements of this and also the given argument.
 int int_size()
          Tells the number of elements in the set.
 boolean isEmpty()
          Is the set empty.
 Object[] toArray()
          Return a new array containing all the elements of this.
 

Method Detail

has

public boolean has(Object elem)
Tell whether the argument is equal to one of the elements in this collection, using the notion of element equality appropriate for the collection.

Specifications: (class)pure
public normal_behavior
requires this.isEmpty();
ensures !\result ;

equals

public boolean equals(nullable Object s2)
Overrides:
equals in class Object
Specifications: (class)pure
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 ;

isEmpty

public boolean isEmpty()
Is the set empty.

See Also:
int_size(), has(Object)
Specifications: (class)pure
public normal_behavior
ensures \result == ( \forall java.lang.Object e; ; !this.has(e));

int_size

public int int_size()
Tells the number of elements in the set.

Specifications: (class)pure
public normal_behavior
ensures this.isEmpty() ==> \result == 0;
ensures \result >= 0;

choose

public Object choose()
Return an arbitrary element of this.

See Also:
isEmpty(), #elements()
Specifications: (class)pure
public normal_behavior
requires !this.isEmpty();
ensures this.has(\result );

insert

public JMLSetType insert(Object elem)
Returns a new set that contains all the elements of this and also the given argument.

See Also:
has(Object), #remove(Object)
Specifications: non_null (class)pure
public normal_behavior
requires this.int_size() < 2147483647||this.has(elem);
ensures \result != null&&( \forall java.lang.Object e; ; \result .has(e) ==> this.has(e)||(e == null&&elem == null)||(e != null&&e.equals(elem)));

toArray

public Object[] toArray()
Return a new array containing all the elements of this.

Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&\result .length == this.int_size()&&( \forall java.lang.Object o; this.has(o); ( \exists int i; ; (o == null&&\result [i] == null)||(o != null&&o.equals(\result [i]))));

JML

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.