diff --git a/specs/java/util/ArrayList.jml b/specs/java/util/ArrayList.jml
index 79698ae4..ee17fc9a 100644
--- a/specs/java/util/ArrayList.jml
+++ b/specs/java/util/ArrayList.jml
@@ -33,6 +33,7 @@ public class ArrayList<E> extends AbstractList<E>
       @                  initialAbstractList() &&
       @                  capacity == initialCapacity &&
       @                  isEmpty() &&
+      @                  !isImmutable &&
       @                  containsNull;
       @ public pure model boolean initialArrayList(int initialCapacity);
       @*/
@@ -68,6 +69,7 @@ public class ArrayList<E> extends AbstractList<E>
       @                     this.get(i) == (c.iterator().nthNextElement(i)));
       @   ensures capacity == c.size()*1.1;
       @   ensures containsNull == c.containsNull;
+      @   ensures !isImmutable;
       @ also
       @  public exceptional_behavior
       @   requires c == null;
@@ -79,7 +81,7 @@ public class ArrayList<E> extends AbstractList<E>
     /*-RAC@  public normal_behavior
       @   assignable objectState;
       @   ensures \not_modified(containsNull,content.theSize,content,
-                                                   theString,theHashCode);
+      @                         isImmutable, theString,theHashCode);
       @   ensures capacity == this.size();
       @*/
     public void trimToSize();
@@ -89,6 +91,7 @@ public class ArrayList<E> extends AbstractList<E>
       @   ensures capacity >= minCapacity;
       @   ensures \not_modified(containsNull,content.theSize,content);
       @   ensures \not_modified(theString,theHashCode);
+      @   ensures \not_modified(isImmutable);
       @*/
     public void ensureCapacity(int minCapacity);
 
diff --git a/specs/java/util/Collection.jml b/specs/java/util/Collection.jml
index 4ede886f..babb0883 100644
--- a/specs/java/util/Collection.jml
+++ b/specs/java/util/Collection.jml
@@ -53,6 +53,12 @@ public interface Collection<E> extends Iterable<E> {
      **/
     //-RAC@ instance ghost public boolean containsNull; in localState;
 
+    /**
+     * True iff collection is specified to be immutable (mutators throw 
+     * UnsupportedOperationException), required by various asImmutable*() 
+     * methods in Collections
+     */
+    //-RAC@ model instance public boolean isImmutable; in localState;
 
     //+OPENJML@ immutable 
     //@ pure
@@ -67,7 +73,7 @@ public interface Collection<E> extends Iterable<E> {
       @*/
 
     //-RAC@ public model non_null instance Content content; in localState;
-    //-RAC@ public invariant content.owner == this;
+    //-RAC@ public invariant isImmutable || content.owner == this;
     //-RAC@ public invariant content.theSize >= 0;
 
     /*-RAC@ public normal_behavior
@@ -168,6 +174,7 @@ public interface Collection<E> extends Iterable<E> {
     /*@ non_null @*/ <T> T[] toArray(/*@non_null*/ T[] a) throws NullPointerException, ArrayStoreException;
 
     /*-RAC@ public normal_behavior
+      @   requires !isImmutable;
       @   requires !containsNull ==> o != null;
       {|
       @   requires containsObject(o);
@@ -186,6 +193,11 @@ public interface Collection<E> extends Iterable<E> {
       @   //ensures (\forall Object oo; o != oo; containsObject(oo) ==> \old(containsObject(oo)));
       @   //ensures \old(containsObject(null)) ==> containsObject(null);
       @   //ensures o != null ==> (containsObject(null) ==> \old(containsObject(null)));
+      @ also
+      @ public exceptional_behavior
+      @   requires isImmutable;
+      @   assignable \nothing;
+      @   signals_only UnsupportedOperationException;
       @*/
     /*+RAC@
       @  public normal_behavior
@@ -206,6 +218,7 @@ public interface Collection<E> extends Iterable<E> {
     boolean add(/*@nullable*/ E o);
 
     /*-RAC@ public behavior
+      @   requires !isImmutable;
       @   requires !containsNull ==> o != null;
       @   assignable content; 
       @   ensures \not_modified(containsNull);
@@ -223,25 +236,33 @@ public interface Collection<E> extends Iterable<E> {
       @ also 
       @
       @ public behavior
+      @   requires !isImmutable;
       @   requires !containsNull ==> o != null;
       @   requires containsObject(o);
       @   assignable content; 
       @   ensures \result;
       @ also public behavior
+      @   requires !isImmutable;
       @   requires !containsNull ==> o != null;
       @   requires !containsObject(o);
       @   assignable content; 
       @   ensures !\result;
       @ also public behavior
+      @   requires !isImmutable;
       @   requires !containsNull ==> o != null;
       @   requires !containsObject(null);
       @   assignable content; 
       @   ensures !containsObject(null);
       @ also public behavior
+      @   requires !isImmutable;
       @   requires !containsNull ==> o != null;
       @   requires o!=null && containsObject(null);
       @   assignable content; 
       @   ensures containsObject(null);
+      @ also public exceptional_behavior
+      @   requires isImmutable;
+      @   assignable \nothing;
+      @   signals_only UnsupportedOperationException;
       @*/
     boolean remove(/*@nullable*/ Object o) throws RuntimeException;
 
@@ -262,6 +283,7 @@ public interface Collection<E> extends Iterable<E> {
     // FIXME - what if c == this in the following calls?
 
     /*-RAC@ public behavior
+      @   requires !isImmutable;
       @   requires c != null;
       @   requires !\key("RAC") ==> !containsNull ==> !c.containsNull;
       @   assignable objectState; 
@@ -272,24 +294,30 @@ public interface Collection<E> extends Iterable<E> {
       @   // FIXME ensures \old(c.contains(null) || contains(null)) <==> contains(null);
           // See note in add about exceptions
       @ also public exceptional_behavior
-      @  requires c == null;
-      @  assignable \nothing;
-      @  signals_only NullPointerException;
+      @   requires !isImmutable;
+      @   requires c == null;
+      @   assignable \nothing;
+      @   signals_only NullPointerException;
+      @ also public exceptional_behavior
+      @   requires isImmutable;
+      @   assignable \nothing;
+      @   signals_only UnsupportedOperationException;
       @*/
               // FIXME - also the optional exceptions
     boolean addAll(/*@non_null*/ Collection<? extends E> c) throws NullPointerException;
 
-    /*@ public behavior
+    /*+RAC@ public behavior
       @   requires c != null;
       @   assignable objectState; 
       @   ensures c == this ==> isEmpty();
           // See note in remove about exceptions       // FIXME - also the optional exceptions
       @ also public exceptional_behavior
-      @  requires c == null;
-      @  assignable \nothing;
-      @  signals_only NullPointerException;
+      @   requires c == null;
+      @   assignable \nothing;
+      @   signals_only NullPointerException;
       @*/
     /*-RAC@ also public behavior
+      @   requires !isImmutable;
       @   requires c != null;
       @   assignable objectState; 
       @   ensures \not_modified(containsNull);
@@ -298,10 +326,19 @@ public interface Collection<E> extends Iterable<E> {
       @   // FIXME ensures (contains(null) || \old(c.contains(null))) <==> \old(contains(null));
       @   ensures content.theSize <= \old(content.theSize);
       @   ensures !\result <==> (content.theSize == \old(content.theSize));
+      @ also public exceptional_behavior
+      @   requires !isImmutable;
+      @   requires c == null;
+      @   assignable \nothing;
+      @   signals_only NullPointerException;
+      @ also public exceptional_behavior
+      @   requires isImmutable;
+      @   assignable \nothing;
+      @   signals_only UnsupportedOperationException;
       @*/
     boolean removeAll(/*@non_null*/ Collection<?> c) throws NullPointerException;
 
-    /*@ public behavior
+    /*+RAC@ public behavior
       @   requires c != null;
       @   assignable objectState; 
       @   ensures c == this ==> !\result;
@@ -312,6 +349,7 @@ public interface Collection<E> extends Iterable<E> {
       @  signals_only NullPointerException;
       @*/
     /*-RAC@ public behavior
+      @   requires !isImmutable;
       @   requires c != null;
       @   assignable objectState; 
       @   ensures \not_modified(containsNull);
@@ -323,16 +361,30 @@ public interface Collection<E> extends Iterable<E> {
       @   ensures !\result <==> (content.theSize == \old(content.theSize));
       @   // FIXME ensures !\result ==> (\forall Object o; contains(o) <==> \old(contains(o)));
       @   // FIXME ensures !\result ==> (contains(null) <==> \old(contains(null)));
+      @ also public exceptional_behavior
+      @   requires c == null;
+      @   requires !isImmutable;
+      @   assignable \nothing;
+      @   signals_only NullPointerException;
+      @ also public exceptional_behavior
+      @   requires isImmutable;
+      @   assignable \nothing;
+      @   signals_only UnsupportedOperationException;
       @*/
     // FIXME - also the optional exceptions
     boolean retainAll(/*@non_null*/ Collection<?> c) throws NullPointerException;
 
     /*-RAC@ public behavior
+      @   requires !isImmutable;
       @   assignable objectState; 
       @   ensures !\key("RAC") ==> \not_modified(containsNull);
       @   ensures isEmpty();
       @   ensures_redundantly size() == 0;
           // FIXME See note in remove about exceptions
+      @ also public exceptional_behavior
+      @   requires isImmutable;
+      @   assignable \nothing;
+      @   signals_only UnsupportedOperationException;
       @*/
     void clear();
 
diff --git a/specs/java/util/Collections.jml b/specs/java/util/Collections.jml
index b88b7107..ca95ba53 100644
--- a/specs/java/util/Collections.jml
+++ b/specs/java/util/Collections.jml
@@ -46,12 +46,40 @@ public class Collections {
 //  public static <T> boolean replaceAll(java.util.List<T>, T, T);
 //  public static int indexOfSubList(java.util.List<?>, java.util.List<?>);
 //  public static int lastIndexOfSubList(java.util.List<?>, java.util.List<?>);
-//  public static <T> java.util.Collection<T> unmodifiableCollection(java.util.Collection<? extends T>);
-//  public static <T> java.util.Set<T> unmodifiableSet(java.util.Set<? extends T>);
+
+    //@ public normal_behavior
+    //@   requires true;
+    //@   ensures \fresh(\result);
+    //-RAC@   ensures \result.isImmutable;
+    //@   ensures \result.content == c.content; // changes to original show
+    //@ pure
+    public static <T> java.util.Collection<T> unmodifiableCollection(java.util.Collection<? extends T> c);
+
+    //@ public normal_behavior
+    //@   requires true;
+    //@   ensures \fresh(\result);
+    //-RAC@   ensures \result.isImmutable;
+    //@   ensures \result.content == s.content; // changes to original show
+    //@ pure
+    public static <T> java.util.Set<T> unmodifiableSet(java.util.Set<? extends T> s);
 //  public static <T> java.util.SortedSet<T> unmodifiableSortedSet(java.util.SortedSet<T>);
 //  public static <T> java.util.NavigableSet<T> unmodifiableNavigableSet(java.util.NavigableSet<T>);
-//  public static <T> java.util.List<T> unmodifiableList(java.util.List<? extends T>);
-//  public static <K, V> java.util.Map<K, V> unmodifiableMap(java.util.Map<? extends K, ? extends V>);
+    
+    //@ public normal_behavior
+    //@   requires true;
+    //@   ensures \fresh(\result);
+    //-RAC@   ensures \result.isImmutable;
+    //@   ensures \result.content == l.content; // changes to original show
+    //@ pure
+    public static <T> java.util.List<T> unmodifiableList(java.util.List<? extends T> l);
+
+    //@ public normal_behavior
+    //@   requires true;
+    //@   ensures \fresh(\result);
+    //-RAC@   ensures \result.isImmutable;
+    //@   ensures \result.content == m.content; // changes to original show
+    //@ pure
+    public static <K, V> java.util.Map<K, V> unmodifiableMap(java.util.Map<? extends K, ? extends V> m);
 //  public static <K, V> java.util.SortedMap<K, V> unmodifiableSortedMap(java.util.SortedMap<K, ? extends V>);
 //  public static <K, V> java.util.NavigableMap<K, V> unmodifiableNavigableMap(java.util.NavigableMap<K, ? extends V>);
 //  public static <T> java.util.Collection<T> synchronizedCollection(java.util.Collection<T>);
@@ -78,11 +106,32 @@ public class Collections {
 //  public static <T> java.util.Iterator<T> emptyIterator();
 //  public static <T> java.util.ListIterator<T> emptyListIterator();
 //  public static <T> java.util.Enumeration<T> emptyEnumeration();
-//  public static final <T> java.util.Set<T> emptySet();
+
+    //@ public normal_behavior
+    //@   requires true;
+    //-RAC@   ensures \result.isImmutable;
+    //@   ensures \result.isEmpty();
+    //@   // javadoc says it need not be fresh
+    //@ pure
+    public static final <T> java.util.Set<T> emptySet();
 //  public static <E> java.util.SortedSet<E> emptySortedSet();
 //  public static <E> java.util.NavigableSet<E> emptyNavigableSet();
-//  public static final <T> java.util.List<T> emptyList();
-//  public static final <K, V> java.util.Map<K, V> emptyMap();
+
+    //@ public normal_behavior
+    //@   requires true;
+    //-RAC@   ensures \result.isImmutable;
+    //@   ensures \result.isEmpty();
+    //@   // javadoc says it need not be fresh
+    //@ pure
+    public static final <T> java.util.List<T> emptyList();
+
+    //@ public normal_behavior
+    //@   requires true;
+    //-RAC@   ensures \result.isImmutable;
+    //@   ensures \result.isEmpty();
+    //@   // javadoc says it need not be fresh
+    //@ pure    
+    public static final <K, V> java.util.Map<K, V> emptyMap();
 //  public static final <K, V> java.util.SortedMap<K, V> emptySortedMap();
 //  public static final <K, V> java.util.NavigableMap<K, V> emptyNavigableMap();
 //  public static <T> java.util.Set<T> singleton(T);
diff --git a/specs/java/util/HashMap.jml b/specs/java/util/HashMap.jml
index b5373b91..d50021cf 100644
--- a/specs/java/util/HashMap.jml
+++ b/specs/java/util/HashMap.jml
@@ -1,5 +1,21 @@
 package java.util;
 
 public class HashMap<K,V> extends AbstractMap<K,V> implements Map<K,V>, Cloneable, java.io.Serializable {
-
+    //@ public normal_behavior
+    //@   ensures initialAbstractMap();
+    //@   ensures !isImmutable;
+    public HashMap();
+    
+    //@ public normal_behavior
+    //@   requires m != null;
+    //@   ensures this.size() == m.size();
+    //@   ensures this.entrySet().equals( m.entrySet() );
+    //@   ensures !isImmutable;
+    //@ also public exceptional_behavior
+    //@   requires m == null;
+    //@   signals_only NullPointerException;
+    //@ pure
+    public HashMap(Map<? extends K, ? extends V> m);
+    
+    // method specifications inherited
 }
diff --git a/specs/java/util/HashSet.jml b/specs/java/util/HashSet.jml
index 1f91e861..5d44921a 100644
--- a/specs/java/util/HashSet.jml
+++ b/specs/java/util/HashSet.jml
@@ -3,18 +3,22 @@ package java.util;
 public class HashSet<E> extends AbstractCollection<E> implements Set<E>, Cloneable, java.io.Serializable {
 
     //@ public normal_behavior ensures true;
+    //-RAC@ ensures !isImmutable;
     //@ pure
     public HashSet();
     
     //@ public normal_behavior ensures true;
+    //-RAC@ ensures !isImmutable;
     //@ pure
     public HashSet(Collection<? extends E> c);
     
     //@ public normal_behavior ensures true;
+    //-RAC@ ensures !isImmutable;
     //@ pure
     public HashSet(int initialCapacity);
     
     //@ public normal_behavior ensures true;
+    //-RAC@ ensures !isImmutable;
     //@ pure
     public HashSet(int initialCapacity, float loadFactor);
     
@@ -37,5 +41,4 @@ public class HashSet<E> extends AbstractCollection<E> implements Set<E>, Cloneab
     //@ also public normal_behavior ensures true;
     //@ pure
     public int size();
-    
 }
diff --git a/specs/java/util/List.jml b/specs/java/util/List.jml
index 64d5ed1a..092516c0 100644
--- a/specs/java/util/List.jml
+++ b/specs/java/util/List.jml
@@ -112,6 +112,7 @@ public interface List<E> extends Collection<E> {
     <T> T[] toArray(T[] a) throws NullPointerException;
 
     /*-RAC@ also public normal_behavior
+      @   requires !isImmutable;
       @   requires !containsNull ==> o != null;
       @   assignable content;
       @   ensures content != null;  // FIXME - not strictly necessary
@@ -126,6 +127,7 @@ public interface List<E> extends Collection<E> {
 
     /*-RAC@
       @ also public normal_behavior
+      @   requires !isImmutable;
       @   requires contains(o);
       @   assignable objectState;
       @   ensures content.theSize == \old(content.theSize-1);
@@ -134,6 +136,7 @@ public interface List<E> extends Collection<E> {
               (\forall \bigint k; 0<=k && k<j; get(content,k) == \old(get(content,k)))
           &&  (\forall \bigint k; j<k && k<content.theSize; get(content,k-1)==\old(get(content,k+1)))); */
     /*-RAC@ also public exceptional_behavior
+      @   requires !isImmutable;
       @   requires !contains(o);
       @   assignable \nothing;
       @   signals_only NoSuchElementException;
@@ -186,6 +189,7 @@ public interface List<E> extends Collection<E> {
 
     /*-RAC@
       @ public behavior
+      @ requires !isImmutable;
       @ requires !containsNull ==> element != null;
       @ {|
       @   requires 0 <= index && index < size();
@@ -214,10 +218,15 @@ public interface List<E> extends Collection<E> {
       @   ensures false;
       @   signals_only IndexOutOfBoundsException;
       @ |}
+      @ also public exceptional_behavior
+      @   requires isImmutable;
+      @   assignable \nothing;
+      @   signals_only UnsupportedOperationException;
       @*/
     E set(int index, E element);
     
     /*-RAC@ public behavior
+      @   requires !isImmutable;
       @   requires !containsNull ==> element != null;
       @   {|
       @     requires  0 <= index && index <= size();
@@ -248,6 +257,10 @@ public interface List<E> extends Collection<E> {
       @   ensures false;
       @   signals_only IndexOutOfBoundsException;
       @ |}
+      @ also public exceptional_behavior
+      @   requires isImmutable;
+      @   assignable \nothing;
+      @   signals_only UnsupportedOperationException;
       @*/
     /*+RAC@ public behavior
       @   requires  0 <= index && index <= size();
@@ -264,6 +277,7 @@ public interface List<E> extends Collection<E> {
     void add(int index, E element);
 
     /*-RAC@ public behavior
+      @   requires !isImmutable;
       @   requires  0 <= index && index < size();
       @   assignable objectState;
       @   ensures \not_modified(containsNull);
@@ -279,9 +293,14 @@ public interface List<E> extends Collection<E> {
       @            (* remove method not supported by list *);
           // FIXME - other exceptions?
       @ also public exceptional_behavior
+      @   requires !isImmutable;
       @   requires !(0 <= index && index < size());
       @   assignable \nothing;
       @   signals_only IndexOutOfBoundsException;
+      @ also public exceptional_behavior
+      @   requires isImmutable;
+      @   assignable \nothing;
+      @   signals_only UnsupportedOperationException;
       @*/
     E remove(int index);
 
diff --git a/specs/java/util/Map.jml b/specs/java/util/Map.jml
index 9b8ea25c..ecb68176 100644
--- a/specs/java/util/Map.jml
+++ b/specs/java/util/Map.jml
@@ -77,7 +77,7 @@ public interface Map<K,V> {
      */
           
     //-RAC@ public model instance non_null Content content; in objectState;
-    //-RAC@ public invariant content.owner == this;
+    //-RAC@ public invariant isImmutable || content.owner == this;
 
     /*-RAC@ public normal_behavior
       @   ensures \result <==> ( 
@@ -150,6 +150,13 @@ public interface Map<K,V> {
           @*/
     }
 
+    /**
+     * True iff map is specified to be immutable (mutators throw 
+     * UnsupportedOperationException), required by various asImmutable*() 
+     * methods in Collections
+     */
+    //-RAC@ model public instance boolean isImmutable;
+
     //@ public normal_behavior
     //@   ensures (* \result == content.theSize *);
     //-RAC@   ensures \result == content.theSize;
@@ -202,6 +209,7 @@ public interface Map<K,V> {
     /*@ pure @*/ V get(Object key);
 
     /*-RAC@ public behavior
+      @    requires !isImmutable;
       @    assignable objectState;
       @    ensures content.hasMap(key);
       @    ensures !isEmpty() && containsKey(key) && containsValue(value);
@@ -232,6 +240,10 @@ public interface Map<K,V> {
                         \old(content.mapsObject(k)) == content.mapsObject(k));
       @    ensures key != null ==> \old(content.mapsObject(null)) 
                                        == content.mapsObject(null);
+      @ also public exceptional_behavior
+      @   requires isImmutable;
+      @   assignable \nothing;
+      @   signals_only UnsupportedOperationException;
       @*/
     /* FIXME @
       @    signals (NullPointerException) \not_modified(value)
@@ -248,6 +260,7 @@ public interface Map<K,V> {
     V put(K key, V value);
 
     /*-RAC@ public behavior
+      @    requires !isImmutable;
       @    assignable objectState;
       @    ensures !content.hasMapObject(key);
       @    ensures !content.hasMap(key);
@@ -268,9 +281,15 @@ public interface Map<K,V> {
       @    signals (NullPointerException) key == null
       @              && (* if this map doesn't support null keys *);
       @*/
+    /*-RAC@ also public exceptional_behavior
+      @   requires isImmutable;
+      @   assignable \nothing;
+      @   signals_only UnsupportedOperationException;
+      @*/
     V remove(Object key);
 
-    /*@ public behavior
+    /*-RAC@ public behavior
+           requires !isImmutable;
            requires t != null;
            assignable objectState;
            ensures \old(isEmpty() && t.isEmpty()) <==> isEmpty();
@@ -281,9 +300,14 @@ public interface Map<K,V> {
            ensures (\forall Object k; \old(containsKey(k) && !t.containsKey(k))
                                               ==> get(k) == \old(get(k)));
         also public exceptional_behavior
+           requires !isImmutable;
            requires t == null;
            assignable \nothing;
            signals_only NullPointerException;
+        also public exceptional_behavior
+          requires isImmutable;
+          assignable \nothing;
+          signals_only UnsupportedOperationException;
       @*/
      /*  FIXME
       @    signals (NullPointerException) \not_modified(theMap)
@@ -300,9 +324,14 @@ public interface Map<K,V> {
     void putAll(Map<? extends K, ? extends V> t);
 
     /*-RAC@ public normal_behavior
-      @    assignable objectState;
-      @    ensures isEmpty();
-      @    ensures (\forall Object k; !content.hasMapObject(k));
+      @   requires !isImmutable;
+      @   assignable objectState;
+      @   ensures isEmpty();
+      @   ensures (\forall Object k; !content.hasMapObject(k));
+      @ also public exceptional_behavior
+      @   requires isImmutable;
+      @   assignable \nothing;
+      @   signals_only UnsupportedOperationException;
       @*/
     void clear();
     
@@ -315,18 +344,18 @@ public interface Map<K,V> {
     //@    ensures \result == _keySet;
     /*@ pure @*/ Set<K> keySet();
 
-    /*@ public normal_behavior 
-      @    ensures \result != null;
-      @    ensures \result.size() >= 0; // FIXME - why needed?
-           // FIXME
-      @*/
+    //@ public normal_behavior 
+    //@    ensures \result != null;
+    //@    ensures \result.size() >= 0; // FIXME - why needed?
+    //-RAC@    ensures isImmutable <==> \result.isImmutable;
+    //@ // FIXME
     /*@ pure @*/ Collection<V> values();
 
-    /*@ public normal_behavior
-      @    ensures \result != null; 
-      @    ensures \result.size() >= 0;  // FIXME - why needed?
-           // FIXME
-      @*/
+    //@ public normal_behavior
+    //@    ensures \result != null; 
+    //@    ensures \result.size() >= 0;  // FIXME - why needed?
+    //-RAC@    ensures isImmutable <==> \result.isImmutable;
+    //@ // FIXME
     /*@ pure @*/ Set<Entry<K,V>> entrySet();
 
     /*@
diff --git a/specs/java/util/Queue.jml b/specs/java/util/Queue.jml
index 58015dc7..3854403a 100644
--- a/specs/java/util/Queue.jml
+++ b/specs/java/util/Queue.jml
@@ -45,6 +45,7 @@ public interface Queue<E> extends Collection<E> {
       @*/
     
     /*-RAC@ also public behavior
+      @   requires !isImmutable;
       @   ensures _get(size()-1) == e && size() == \old(size())+1;
       @   ensures (\forall \bigint i; 0 <= i & i < content.theSize-1; _get(i) == \old(_get(i)));
       @   ensures \result;
@@ -96,6 +97,7 @@ public interface Queue<E> extends Collection<E> {
       @   assignable \nothing;
       @ also
       @ public normal_behavior
+      @   requires !isImmutable;
       @   requires !isEmpty();
       @   ensures \result == \old(_get(0));
       @   ensures (\forall \bigint i; 0 < i & i < content.theSize; _get(i-1) == \old(_get(i)));
@@ -110,6 +112,7 @@ public interface Queue<E> extends Collection<E> {
       @   assignable \nothing;
       @ also
       @ public normal_behavior
+      @   requires !isImmutable;
       @   requires !isEmpty();
       @   ensures \result == \old(_get(0));
       @   ensures (\forall \bigint i; 0 < i & i < content.theSize; _get(i-1) == \old(_get(i)));
diff --git a/specs/java/util/Set.jml b/specs/java/util/Set.jml
index c60ec0b5..819fdb74 100644
--- a/specs/java/util/Set.jml
+++ b/specs/java/util/Set.jml
@@ -57,14 +57,15 @@ public interface Set<E> extends Collection<E> {
     //-RAC@   ensures this.content.owner == \old(this.content.owner);
     boolean add(/*@nullable*/ E o);
 
-    /*@ also
-       @ public normal_behavior
-       @   requires contains(o);
-       @   assignable objectState;
-       @   ensures \result;
-       @   ensures !contains(o);
-       @*/
+    //@ also
+    //@ public normal_behavior
+    //-RAC@   requires !isImmutable;
+    //@   requires contains(o);
+    //@   assignable objectState;
+    //@   ensures \result;
+    //@   ensures !contains(o);
     //@ also public behavior
+    //-RAC@   requires !isImmutable;
     //-RAC@   requires !containsNull ==> o != null;
     //@   requires !contains(o);
     //@   assignable \nothing; 
@@ -83,15 +84,14 @@ public interface Set<E> extends Collection<E> {
     // specs are inherited
     boolean retainAll(/*@non_null*/ Collection<?> c) throws NullPointerException;
 
-    /*@ also public normal_behavior
-       @   requires c != null;
-       @   assignable objectState;
-       @   ensures \old(c.contains(null)) ==> !contains(null);
-       @   ensures (\forall Object o; c.contains(o) <==>
-                      (\old(contains(o)) && !\old(c.contains(o))));
-       @   ensures size() <= \old(size());
-       @   ensures \result <==> size() != \old(size());
-       @*/
+    //@ also public normal_behavior
+    //-RAC@ requires !isImmutable; 
+    //@   requires c != null;
+    //@   assignable objectState;
+    //@   ensures \old(c.contains(null)) ==> !contains(null);
+    //@   ensures (\forall Object o; c.contains(o) <==> (\old(contains(o)) && !\old(c.contains(o))));
+    //@   ensures size() <= \old(size());
+    //@   ensures \result <==> size() != \old(size());
     boolean removeAll(/*@non_null*/ Collection<?> c) throws NullPointerException;
 
     // specification inherited
diff --git a/specs/java/util/Vector.jml b/specs/java/util/Vector.jml
index 4ccc37e8..afdc3115 100644
--- a/specs/java/util/Vector.jml
+++ b/specs/java/util/Vector.jml
@@ -71,6 +71,7 @@ public class Vector<E> extends AbstractList<E>
       @    ensures containsNull;
       @    ensures isEmpty();
       @    ensures elementCount == 0;
+      @    ensures !isImmutable;
       @*/
     public /*@ pure @*/ Vector (int initialCapacity, int capacityIncrement);
 
@@ -81,6 +82,7 @@ public class Vector<E> extends AbstractList<E>
       @    ensures containsNull;
       @    ensures isEmpty();
       @    ensures elementCount == 0;
+      @    ensures !isImmutable;
       @*/
     public /*@ pure @*/ Vector(int initialCapacity);
 
@@ -95,6 +97,7 @@ public class Vector<E> extends AbstractList<E>
 
     /*@ public normal_behavior
       @    requires c != null;
+      @    ensures !isImmutable;
       @    ensures elementCount == c.size();
       @    ensures this.containsNull == c.containsNull;
       @    ensures this.content.theSize == c.content.theSize;
@@ -120,6 +123,7 @@ public class Vector<E> extends AbstractList<E>
                // theHashCode is not changed because the result does not
                // change equals
       @    ensures \not_modified(elementCount,containsNull);
+      @    ensures \not_modified(isImmutable);
       @    ensures \not_modified(content.theSize);
       @    ensures (\forall int i; 0<=i && i<size(); get(i) == \old(get(i)));
       @    ensures maxCapacity == elementCount;
@@ -134,6 +138,7 @@ public class Vector<E> extends AbstractList<E>
     //@  also
     //@    requires minCapacity > maxCapacity;
     //@    assignable objectState;
+    //-RAC@    ensures \not_modified(isImmutable);
     //-RAC@    ensures \not_modified(theString,theHashCode);
     //@           // theHashCode is not changed because the result does not
     //@           // changes equals
@@ -163,6 +168,7 @@ public class Vector<E> extends AbstractList<E>
       @    ensures elementCount == newSize; */
     /*-RAC@    ensures \not_modified(theString,theHashCode);
       @    ensures \not_modified(containsNull);
+      @   ensures \not_modified(isImmutable);
       @   ensures (\forall int i; 0<=i && i<elementCount;
       @            elementData[i] == \old(elementData[i])); */
     //@  also