// @(#)$Id: JMLSequence.java-generic,v 1.81 2008/10/24 18:07:50 smshaner Exp $ // Copyright (C) 2005 Iowa State University // // This file is part of the runtime library of the Java Modeling Language. // // This library is free software; you can redistribute it and/or // modify it under the terms of the GNU Lesser General Public License // as published by the Free Software Foundation; either version 2.1, // of the License, or (at your option) any later version. // // This library is distributed in the hope that it will be useful, // but WITHOUT ANY WARRANTY; without even the implied warranty of // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU // Lesser General Public License for more details. // // You should have received a copy of the GNU Lesser General Public License // along with JML; see the file LesserGPL.txt. If not, write to the Free // Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA // 02110-1301 USA. package org.jmlspecs.models; import java.math.BigInteger; /** Sequences of objects. This type uses ".equals" * to compare elements, and does not clone elements that are passed into * and returned from the sequence's methods. * *
The informal model for a JMLEqualsSequence is a finite
* mathematical sequence of elements (of type {@link Object}). In
* some examples, we will write
* <a,b,c> for a mathematical
* sequence of length 3, containing elements a, b,
* and c. Elements of sequences are "indexed" from 0, so the
* length of a sequence is always 1 more than the index of the last
* element in the sequence.
*
* @version $Revision: 1.81 $
* @author Gary T. Leavens
* @author Albert L. Baker
* @see JMLCollection
* @see JMLType
* @see JMLObjectSequence
* @see JMLValueSequence
* @see JMLEqualsSequenceEnumerator
*
*/
//-@ immutable
// FIXME: adapt this file to non-null-by-default and remove the following modifier.
/*@ nullable_by_default @*/
public /*@ pure @*/ class JMLEqualsSequence
implements JMLCollection
{
//*********************** equational theory ***********************
/*@ public invariant (\forall JMLEqualsSequence s2;
@ (\forall Object e1, e2;
@ (\forall \bigint n;
@ equational_theory(this, s2, e1, e2, n) )));
@*/
/** An equational specification of the properties of sequences.
*/
/*@ public normal_behavior
@ {|
@ // The following are defined by observations (itemAt) and induction.
@
@ ensures \result <==> !(new JMLEqualsSequence()).has(e1);
@ also
@ ensures \result <==> (new JMLEqualsSequence()).size() == 0;
@ also
@ ensures \result <==> (new JMLEqualsSequence(e1)).size() == 1;
@ also
@ ensures \result <==>
@ e1 != null ==>
@ (new JMLEqualsSequence(e1)).itemAt(0) .equals(e1);
@ also
@ ensures \result <==>
@ e1 != null ==>
@ s.insertFront(e1).first() .equals(e1);
@ also
@ ensures \result <==>
@ e1 != null ==>
@ s.insertBack(e1).last() .equals(e1);
@ also
@ ensures \result <==>
@ e1 != null ==>
@ s.insertFront(e1).itemAt(0) .equals(e1);
@ also
@ ensures \result <==>
@ s.insertFront(e1).size() == s.size() + 1;
@ also
@ ensures \result <==>
@ e1 != null ==>
@ s.insertBack(e1).itemAt(s.size()) .equals(e1);
@ also
@ ensures \result <==>
@ s.insertBack(e1).size() == s.size() + 1;
@ also
@ ensures \result <==>
@ // !FIXME! The following may be inconsistent: argument to itemAt might
@ // be equal to size, but it is required to be less than size.
@ -1 <= n && n < s.size() && e1 != null
@ ==> s.insertAfterIndex(n, e1).itemAt(n+1) .equals(e1);
@ also
@ ensures \result <==>
@ -1 <= n && n < s.size()
@ ==> s.insertAfterIndex(n, e1).size() == s.size() + 1;
@ also
@ ensures \result <==>
@ 0 <= n && n <= s.size() && e1 != null
@ ==> s.insertBeforeIndex(n, e1).itemAt(n) .equals(e1);
@ also
@ ensures \result <==>
@ 0 <= n && n <= s.size()
@ ==> s.insertBeforeIndex(n, e1).size() == s.size() + 1;
@ also
@ ensures \result <==>
@ s.isPrefix(s2)
@ == (\forall int i; 0 <= i && i < s.int_length();
@ (s2.itemAt(i) != null
@ && s2.itemAt(i) .equals(s.itemAt(i)))
@ || (s2.itemAt(i) == null && s.itemAt(i) == null) );
@ also
@ ensures \result <==>
@ s.isSubsequence(s2)
@ == s.int_length() <= s2.int_length()
@ && (s.isPrefix(s2) || s.isSubsequence(s2.trailer()) );
@
@ // The following are all defined as abbreviations.
@
@ also
@ ensures \result <==>
@ s.isEmpty() == (s.size() == 0);
@ also
@ ensures \result <==>
@ s.isEmpty() == (s.length == 0);
@ also
@ ensures \result <==>
@ (new JMLEqualsSequence(e1)).equals(
@ new JMLEqualsSequence().insertFront(e1));
@ also
@ ensures \result <==>
@ (new JMLEqualsSequence(e1)).equals(
@ new JMLEqualsSequence().insertBack(e1));
@ also
@ ensures \result <==>
@ (new JMLEqualsSequence(e1)).equals(
@ new JMLEqualsSequence().insertAfterIndex(-1, e1));
@ also
@ ensures \result <==>
@ (new JMLEqualsSequence(e1)).equals(
@ new JMLEqualsSequence().insertBeforeIndex(0, e1));
@ also
@ ensures \result <==>
@ (s.size() >= 1 ==> s.equals(s.trailer().insertFront(s.first())));
@ also
@ ensures \result <==>
@ (s.size() >= 1 ==> s.equals(s.header().insertBack(s.last())));
@ also
@ ensures \result <==>
@ s.isProperSubsequence(s2)
@ == ( s.isSubsequence(s2) && !s.equals(s2));
@ also
@ ensures \result <==>
@ s.isSupersequence(s2) == s2.isSubsequence(s);
@ also
@ ensures \result <==>
@ s.isProperSupersequence(s2) == s2.isProperSubsequence(s);
@ |}
@
@ // other ways to specify some operations
@ implies_that
@ ensures \result <==> (new JMLEqualsSequence()).isEmpty();
public pure model boolean equational_theory(JMLEqualsSequence s,
JMLEqualsSequence s2,
Object e1,
Object e2, \bigint n);
@*/
//@ public invariant elementType <: \type(Object);
/*@ public invariant
@ (\forall Object o; o != null && has(o);
@ \typeof(o) <: elementType);
@*/
//@ public invariant_redundantly isEmpty() ==> !containsNull;
/** The list representing this sequence's elements, in order.
*/
protected final JMLListEqualsNode theSeq;
//@ in objectState;
//@ maps theSeq.elementState \into elementState;
//@ invariant theSeq != null ==> theSeq.owner == this;
/** This sequence's length.
*/
protected final BigInteger _length;
//@ in objectState;
//@ public model \bigint length;
//@ protected represents length <- bigIntegerToBigint(_length);
//@ protected invariant theSeq == null <==> length == 0;
//@ protected invariant length >= 0;
/*@ protected invariant theSeq != null ==> length == theSeq.length();
@ protected invariant length == length();
@*/
//@ public invariant owner == null;
//************************* Constructors ********************************
/** Initialize this to be the empty sequence.
* @see #EMPTY
*/
/*@ public normal_behavior
@ assignable objectState, elementType, containsNull, owner;
@ ensures isEmpty();
@ ensures_redundantly size() == 0;
@ ensures_redundantly (* this is an empty sequence *);
@*/
//@ implies_that
//@ ensures elementType <: \type(Object) && !containsNull;
public JMLEqualsSequence() {
//@ set owner = null;
theSeq = null;
_length = BigInteger.ZERO;
//@ set elementType = \type(Object);
//@ set containsNull = false;
}
/** Initialize this to be the sequence containing just the given element.
* @param e the element that is the first element in this sequence.
* @see #singleton
*/
public JMLEqualsSequence (Object e)
/*@ public normal_behavior
@ assignable objectState, elementType, containsNull, owner;
@ ensures int_length() == 1;
@ ensures (e == null ==> itemAt(0) == null)
@ && (e != null ==> itemAt(0) .equals(e));
@ ensures_redundantly
@ (* this is a sequence containing just e *);
@*/
{
//@ set owner = null;
theSeq = JMLListEqualsNode.cons(e, null); // cons() clones e, if needed
_length = BigInteger.ONE;
//@ set elementType = (e == null ? \type(Object) : \typeof(e));
//@ set containsNull = (e == null);
//@ set theSeq.owner = this;
}
/** Initialize this sequence based on the given representation.
*/
//@ requires ls == null <==> len == 0;
//@ requires len >= 0;
//@ assignable objectState, elementType, containsNull, owner;
//@ ensures ls != null ==> elementType == ls.elementType;
//@ ensures ls != null ==> containsNull == ls.containsNull;
//@ ensures ls == null ==> elementType <: \type(Object);
//@ ensures ls == null ==> !containsNull;
/*@
model protected JMLEqualsSequence (JMLListEqualsNode ls, \bigint len) {
//@ set owner = null;
theSeq = ls;
_length = bigintToBigInteger(len);
//@ set elementType = ((ls == null) ? \type(Object) : ls.elementType);
//@ set containsNull = ((ls == null) ? false : ls.containsNull);
//@ set theSeq.owner = this;
}@*/
/** Initialize this sequence based on the given representation.
*/
//@ requires ls == null <==> len == 0;
//@ requires len >= 0;
//@ assignable objectState, elementType, containsNull, owner;
//@ ensures ls != null ==> elementType == ls.elementType;
//@ ensures ls != null ==> containsNull == ls.containsNull;
//@ ensures ls == null ==> elementType <: \type(Object);
//@ ensures ls == null ==> !containsNull;
protected JMLEqualsSequence (JMLListEqualsNode ls, int len) {
//@ set owner = null;
theSeq = ls;
_length = BigInteger.valueOf(len);
/*@ set elementType = ((ls == null) ? \type(Object)
@ : ls.elementType);
@*/
//@ set containsNull = ((ls == null) ? false : ls.containsNull);
}
//**************************** Static methods ****************************
/** The empty JMLEqualsSequence.
* @see #JMLEqualsSequence()
*/
public static final /*@ non_null @*/ JMLEqualsSequence EMPTY
= new JMLEqualsSequence();
/** Return the singleton sequence containing the given element.
* @see #JMLEqualsSequence(Object)
*/
/*@ public normal_behavior
@ assignable \nothing;
@ ensures \result != null && \result.equals(new JMLEqualsSequence(e));
@*/
public static /*@ pure @*/ /*@ non_null @*/
JMLEqualsSequence singleton(Object e)
{
return new JMLEqualsSequence(e);
}
/** Return the sequence containing all the elements in the given
* array in the same order as the elements appear in the array.
*/
/*@ public normal_behavior
@ requires a != null;
@ assignable \nothing;
@ ensures \result != null && \result.size() == a.length
@ && (\forall int i; 0 <= i && i < a.length;
@ (\result.itemAt(i) == null
@ ? a[i] == null
@ : \result.itemAt(i) .equals(a[i])));
@*/
public static /*@ pure @*/ /*@ non_null @*/
JMLEqualsSequence convertFrom(/*@ non_null @*/Object[] a)
{
/*@ non_null @*/ JMLEqualsSequence ret = EMPTY;
for (int i = a.length-1; 0 <= i; i--) {
ret = ret.insertFront(a[i]);
}
return ret;
} //@ nowarn Exception;
/** Return the sequence containing the first 'size' elements in the given
* array in the same order as the elements appear in the array.
*/
/*@ public normal_behavior
@ requires a != null && 0 <= size && size < a.length;
@ assignable \nothing;
@ ensures \result != null && \result.size() == size
@ && (\forall int i; 0 <= i && i < size;
@ (\result.itemAt(i) == null
@ ? a[i] == null
@ : \result.itemAt(i) .equals(a[i])));
@
@ implies_that
@ requires size < a.length;
@*/
public static /*@ pure @*/ /*@ non_null @*/
JMLEqualsSequence convertFrom(/*@ non_null @*/Object[] a, int size)
{
/*@ non_null @*/ JMLEqualsSequence ret = EMPTY;
for (int i = size-1; 0 <= i; i--) {
ret = ret.insertFront(a[i]);
}
return ret;
} //@ nowarn Exception;
/** Return the sequence containing all the object in the
* given collection in the same order as the elements appear in the
* collection.
*
* @throws ClassCastException if some element in c is not an instance of
* Object.
* @see #containsAll(java.util.Collection)
*/
/*@ public normal_behavior
@ requires c != null
@ && c.elementType <: \type(Object);
@ requires c.size() < Integer.MAX_VALUE;
@ assignable \nothing;
@ ensures \result != null && \result.size() == c.size()
@ && (\forall Object x; c.contains(x) <==> \result.has(x))
@ && (* the elements in \result are in the same order as c *);
@ also
@ public exceptional_behavior
@ requires c != null && (\exists Object o; c.contains(o);
@ !(o instanceof Object));
@ assignable \nothing;
@ signals_only ClassCastException;
@*/
public static /*@ pure @*/ /*@ non_null @*/
JMLEqualsSequence convertFrom(/*@ non_null @*/ java.util.Collection c)
throws ClassCastException
{
/*@ non_null @*/ JMLEqualsSequence ret = EMPTY;
java.util.Iterator celems = c.iterator();
while (celems.hasNext()) {
Object o = celems.next();
if (o == null) {
ret = ret.insertBack(null);
} else {
//@ assume o instanceof Object;
ret = ret.insertBack(o);
}
}
return ret;
} //@ nowarn Exception;
/** Return the sequence containing all the object in the
* given JMLCollection in the same order as the elements appear in the
* collection.
*
* @throws ClassCastException if some element in c is not an instance of
* Object.
*/
/*@ public normal_behavior
@ requires c != null
@ && c.elementType <: \type(Object);
@ requires c.size() < Integer.MAX_VALUE;
@ assignable \nothing;
@ ensures \result != null
@ && (\forall Object x; c.has(x) <==> \result.has(x))
@ && (* the elements in \result are in the same order as c *);
@ ensures_redundantly \result.size() == c.size();
@ also
@ public exceptional_behavior
@ requires c != null && (\exists Object o; c.has(o);
@ !(o instanceof Object));
@ assignable \nothing;
@ signals_only ClassCastException;
@*/
public static /*@ pure @*/ /*@ non_null @*/
JMLEqualsSequence convertFrom(/*@ non_null @*/ JMLCollection c)
throws ClassCastException
{
/*@ non_null @*/ JMLEqualsSequence ret = EMPTY;
JMLIterator celems = c.iterator();
while (celems.hasNext()) {
Object o = celems.next();
if (o == null) {
ret = ret.insertBack(null);
} else {
//@ assume o instanceof Object;
ret = ret.insertBack(o);
}
}
return ret;
} //@ nowarn Exception;
//**************************** Observers **********************************
/** Return the element at the given zero-based index.
* @param i the zero-based index into the sequence.
* @exception JMLSequenceException if the index oBiI is out of range.
* @see #get(int)
* @see #has(Object)
* @see #count(Object)
*/
/*@ // _ alsoIfValue _ //FIXME! later
@ public normal_behavior
@ requires 0 <= i && i < length;
@ ensures
@ (* \result == null, if the ith element of this is null;
@ otherwise, \result ".equals" the ith element of this *);
@ ensures \result != null ==> \typeof(\result) <: elementType;
@ ensures !containsNull ==> \result != null;
@ also
@ public exceptional_behavior
@ requires !(0 <= i && i < length);
@ signals_only JMLSequenceException;
@ for_example
@ public normal_example
@ requires (* this is