Skip to content

Have immutable flag to allow for returning unmodifiable collections in java.util.Collections #8

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
slyubomirsky wants to merge 10 commits into
base: development
Choose a base branch
from
Open

Have immutable flag to allow for returning unmodifiable collections in java.util.Collections #8

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
893285c
Add immutable flag to various java.util collections classes to allow …
Aug 16, 2018
82a48df
Add specifications for empty*() methods in java.util.Collections
Aug 17, 2018
efbd85a
Add specs for HashMap constructors for good measure
Aug 17, 2018
8d2347c
Correct variable names in HashMap
Aug 17, 2018
3c4faa6
Check for null in HashMap constructor
Aug 17, 2018
eef1565
Avoid using quantifiers to specify HashMap constructor (catastrophic …
Aug 17, 2018
8952e2c
isImmutable is model field, keep it in -RAC blocks
Aug 22, 2018
5b18e8c
Fix merge conflict by switching tabs to spaces in HashSet.jml
Aug 29, 2018
b23d3c5
Remove invariants about isImmutable, assert in constructors & methods…
Sep 6, 2018
18a2c30
Update content owner invariant to mention immutability
Sep 6, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 4 additions & 1 deletion specs/java/util/ArrayList.jml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@ public class ArrayList<E> extends AbstractList<E>
@ initialAbstractList() &&
@ capacity == initialCapacity &&
@ isEmpty() &&
@ !isImmutable &&
@ containsNull;
@ public pure model boolean initialArrayList(int initialCapacity);
@*/
Expand Down Expand Up @@ -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;
Expand All @@ -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();
Expand All @@ -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);

Expand Down
70 changes: 61 additions & 9 deletions specs/java/util/Collection.jml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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);
Expand All @@ -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
Expand All @@ -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);
Expand All @@ -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;

Expand All @@ -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;
Expand All @@ -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);
Expand All @@ -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;
Expand All @@ -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);
Expand All @@ -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();

Expand Down
63 changes: 56 additions & 7 deletions specs/java/util/Collections.jml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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>);
Expand All @@ -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);
Expand Down
18 changes: 17 additions & 1 deletion specs/java/util/HashMap.jml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
}
5 changes: 4 additions & 1 deletion specs/java/util/HashSet.jml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);

Expand All @@ -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();

}
Loading