From 893285c565de55bb6621e204ebb6d2eeb14fbd7c Mon Sep 17 00:00:00 2001 From: Steven Lyubomirsky Date: Thu, 16 Aug 2018 16:44:17 -0700 Subject: [PATCH 01/10] Add immutable flag to various java.util collections classes to allow for returning unmodifiable collections in java.util.Collecitons --- specs/java/util/ArrayList.jml | 2 + specs/java/util/Collection.jml | 68 +++++++++++++++++++++++++++++---- specs/java/util/Collections.jml | 36 +++++++++++++++-- specs/java/util/HashMap.jml | 2 +- specs/java/util/HashSet.jml | 25 ++++++------ specs/java/util/List.jml | 19 +++++++++ specs/java/util/Map.jml | 37 ++++++++++++++++-- specs/java/util/Queue.jml | 2 + specs/java/util/Set.jml | 32 ++++++++-------- specs/java/util/Vector.jml | 1 + 10 files changed, 180 insertions(+), 44 deletions(-) diff --git a/specs/java/util/ArrayList.jml b/specs/java/util/ArrayList.jml index 79698ae4..2f884052 100644 --- a/specs/java/util/ArrayList.jml +++ b/specs/java/util/ArrayList.jml @@ -43,6 +43,8 @@ public class ArrayList extends AbstractList /*@ public model int capacity; in objectState; @*/ + //@ public invariant !isImmutable; + // METHODS AND CONSTRUCTORS //@ public normal_behavior //@ requires 0 <= initialCapacity; diff --git a/specs/java/util/Collection.jml b/specs/java/util/Collection.jml index 4ede886f..104c726d 100644 --- a/specs/java/util/Collection.jml +++ b/specs/java/util/Collection.jml @@ -53,6 +53,12 @@ public interface Collection extends Iterable { **/ //-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@ instance ghost public boolean isImmutable; in localState; //+OPENJML@ immutable //@ pure @@ -168,6 +174,7 @@ public interface Collection extends Iterable { /*@ non_null @*/ 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 extends Iterable { @ //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 extends Iterable { 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 extends Iterable { @ 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 extends Iterable { // 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 extends Iterable { @ // 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 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 extends Iterable { @ // 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 extends Iterable { @ signals_only NullPointerException; @*/ /*-RAC@ public behavior + @ requires !isImmutable; @ requires c != null; @ assignable objectState; @ ensures \not_modified(containsNull); @@ -323,16 +361,30 @@ public interface Collection extends Iterable { @ 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..0431186a 100644 --- a/specs/java/util/Collections.jml +++ b/specs/java/util/Collections.jml @@ -46,12 +46,40 @@ public class Collections { // public static boolean replaceAll(java.util.List, T, T); // public static int indexOfSubList(java.util.List, java.util.List); // public static int lastIndexOfSubList(java.util.List, java.util.List); -// public static java.util.Collection unmodifiableCollection(java.util.Collection); -// public static java.util.Set unmodifiableSet(java.util.Set); + + //@ public normal_behavior + //@ requires true; + //@ ensures \fresh(\result); + //@ ensures \result.isImmutable; + //@ ensures \result.content == c.content; // changes to original show + //@ pure + public static java.util.Collection unmodifiableCollection(java.util.Collection c); + + //@ public normal_behavior + //@ requires true; + //@ ensures \fresh(\result); + //@ ensures \result.isImmutable; + //@ ensures \result.content == s.content; // changes to original show + //@ pure + public static java.util.Set unmodifiableSet(java.util.Set s); // public static java.util.SortedSet unmodifiableSortedSet(java.util.SortedSet); // public static java.util.NavigableSet unmodifiableNavigableSet(java.util.NavigableSet); -// public static java.util.List unmodifiableList(java.util.List); -// public static java.util.Map unmodifiableMap(java.util.Map); + + //@ public normal_behavior + //@ requires true; + //@ ensures \fresh(\result); + //@ ensures \result.isImmutable; + //@ ensures \result.content == l.content; // changes to original show + //@ pure + public static java.util.List unmodifiableList(java.util.List l); + + //@ public normal_behavior + //@ requires true; + //@ ensures \fresh(\result); + //@ ensures \result.isImmutable; + //@ ensures \result.content == m.content; // changes to original show + //@ pure + public static java.util.Map unmodifiableMap(java.util.Map m); // public static java.util.SortedMap unmodifiableSortedMap(java.util.SortedMap); // public static java.util.NavigableMap unmodifiableNavigableMap(java.util.NavigableMap); // public static java.util.Collection synchronizedCollection(java.util.Collection); diff --git a/specs/java/util/HashMap.jml b/specs/java/util/HashMap.jml index b5373b91..65a044e3 100644 --- a/specs/java/util/HashMap.jml +++ b/specs/java/util/HashMap.jml @@ -1,5 +1,5 @@ package java.util; public class HashMap extends AbstractMap implements Map, Cloneable, java.io.Serializable { - + //@ public invariant !isImmutable; } diff --git a/specs/java/util/HashSet.jml b/specs/java/util/HashSet.jml index 1f91e861..98b7f45b 100644 --- a/specs/java/util/HashSet.jml +++ b/specs/java/util/HashSet.jml @@ -2,40 +2,41 @@ package java.util; public class HashSet extends AbstractCollection implements Set, Cloneable, java.io.Serializable { + //@ public invariant !isImmutable; + //@ public normal_behavior ensures true; //@ pure public HashSet(); - + //@ public normal_behavior ensures true; //@ pure public HashSet(Collection c); - + //@ public normal_behavior ensures true; //@ pure public HashSet(int initialCapacity); - + //@ public normal_behavior ensures true; //@ pure public HashSet(int initialCapacity, float loadFactor); - + public boolean add(E e); - + public void clear(); - + public Object clone(); - + public boolean contains(Object o); - + //@ also public normal_behavior ensures true; //@ pure public boolean isEmpty(); - + public Iterator iterator(); - + public boolean remove(Object o); - + //@ 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 extends Collection { 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 extends Collection { /*-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 extends Collection { (\forall \bigint k; 0<=k && k extends Collection { /*-RAC@ @ public behavior + @ requires !isImmutable; @ requires !containsNull ==> element != null; @ {| @ requires 0 <= index && index < size(); @@ -214,10 +218,15 @@ public interface List extends Collection { @ 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 extends Collection { @ 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 extends Collection { 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 extends Collection { @ (* 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..4a32d29b 100644 --- a/specs/java/util/Map.jml +++ b/specs/java/util/Map.jml @@ -150,6 +150,13 @@ public interface Map { @*/ } + /** + * True iff map is specified to be immutable (mutators throw + * UnsupportedOperationException), required by various asImmutable*() + * methods in Collections + */ + //-RAC@ public instance ghost boolean isImmutable; + //@ public normal_behavior //@ ensures (* \result == content.theSize *); //-RAC@ ensures \result == content.theSize; @@ -202,6 +209,7 @@ public interface Map { /*@ 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 { \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 { 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 { @ signals (NullPointerException) key == null @ && (* if this map doesn't support null keys *); @*/ + /*@ also public exceptional_behavior + @ requires isImmutable; + @ assignable \nothing; + @ signals_only UnsupportedOperationException; + @*/ V remove(Object key); /*@ public behavior + requires !isImmutable; requires t != null; assignable objectState; ensures \old(isEmpty() && t.isEmpty()) <==> isEmpty(); @@ -281,9 +300,14 @@ public interface Map { 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 { void putAll(Map 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(); @@ -318,6 +347,7 @@ public interface Map { /*@ public normal_behavior @ ensures \result != null; @ ensures \result.size() >= 0; // FIXME - why needed? + @ ensures isImmutable <==> \result.isImmutable; // FIXME @*/ /*@ pure @*/ Collection values(); @@ -325,6 +355,7 @@ public interface Map { /*@ public normal_behavior @ ensures \result != null; @ ensures \result.size() >= 0; // FIXME - why needed? + @ ensures isImmutable <==> \result.isImmutable; // FIXME @*/ /*@ pure @*/ Set> entrySet(); diff --git a/specs/java/util/Queue.jml b/specs/java/util/Queue.jml index 58015dc7..7dc0b769 100644 --- a/specs/java/util/Queue.jml +++ b/specs/java/util/Queue.jml @@ -28,6 +28,8 @@ package java.util; public interface Queue extends Collection { + //@ public invariant !isImmutable; + /*-RAC@ public normal_behavior @ requires n >= 0 && n < content.theSize; @ ensures !\fresh(\result); 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 extends Collection { //-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 extends Collection { // 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..c45edd8f 100644 --- a/specs/java/util/Vector.jml +++ b/specs/java/util/Vector.jml @@ -55,6 +55,7 @@ public class Vector extends AbstractList protected /*@ spec_public @*/ int elementCount; //@ in objectState; + //@ public invariant !isImmutable; //@ public invariant 0 <= elementCount; // I'm commenting out the following, since this is guaranteed by the postcondition of size() From 82a48df8902ee3659a5e95297b92db5d2a75db3f Mon Sep 17 00:00:00 2001 From: Steven Lyubomirsky Date: Fri, 17 Aug 2018 11:02:19 -0700 Subject: [PATCH 02/10] Add specifications for empty*() methods in java.util.Collections --- specs/java/util/Collections.jml | 27 ++++++++++++++++++++++++--- 1 file changed, 24 insertions(+), 3 deletions(-) diff --git a/specs/java/util/Collections.jml b/specs/java/util/Collections.jml index 0431186a..4d0b035f 100644 --- a/specs/java/util/Collections.jml +++ b/specs/java/util/Collections.jml @@ -106,11 +106,32 @@ public class Collections { // public static java.util.Iterator emptyIterator(); // public static java.util.ListIterator emptyListIterator(); // public static java.util.Enumeration emptyEnumeration(); -// public static final java.util.Set emptySet(); + + //@ public normal_behavior + //@ requires true; + //@ ensures \result.isImmutable; + //@ ensures \result.isEmpty(); + //@ // javadoc says it need not be fresh + //@ pure + public static final java.util.Set emptySet(); // public static java.util.SortedSet emptySortedSet(); // public static java.util.NavigableSet emptyNavigableSet(); -// public static final java.util.List emptyList(); -// public static final java.util.Map emptyMap(); + + //@ public normal_behavior + //@ requires true; + //@ ensures \result.isImmutable; + //@ ensures \result.isEmpty(); + //@ // javadoc says it need not be fresh + //@ pure + public static final java.util.List emptyList(); + + //@ public normal_behavior + //@ requires true; + //@ ensures \result.isImmutable; + //@ ensures \result.isEmpty(); + //@ // javadoc says it need not be fresh + //@ pure + public static final java.util.Map emptyMap(); // public static final java.util.SortedMap emptySortedMap(); // public static final java.util.NavigableMap emptyNavigableMap(); // public static java.util.Set singleton(T); From efbd85abc949e01b6afaf885c276d957e7a62f00 Mon Sep 17 00:00:00 2001 From: Steven Lyubomirsky Date: Fri, 17 Aug 2018 11:48:59 -0700 Subject: [PATCH 03/10] Add specs for HashMap constructors for good measure --- specs/java/util/HashMap.jml | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/specs/java/util/HashMap.jml b/specs/java/util/HashMap.jml index 65a044e3..7de68c2b 100644 --- a/specs/java/util/HashMap.jml +++ b/specs/java/util/HashMap.jml @@ -2,4 +2,17 @@ package java.util; public class HashMap extends AbstractMap implements Map, Cloneable, java.io.Serializable { //@ public invariant !isImmutable; + + //@ public normal_behavior + //@ ensures initialAbstractMap(); + public HashMap(); + + //@ public normal_behavior + //@ ensures this.theSize == m.theSize; + //@ ensures (\forall Object o; this.containsKey(k) <==> m.containsKey(k)); + //@ ensures (\forall Object o; m.containsKey(k); this.containsKey(k) && this.get(k) == m.get(k)); + //@ pure + public HashMap(Map m); + + // method specifications inherited } From 8d2347c855c76b57d7072f369827673574969b3f Mon Sep 17 00:00:00 2001 From: Steven Lyubomirsky Date: Fri, 17 Aug 2018 14:47:36 -0700 Subject: [PATCH 04/10] Correct variable names in HashMap --- specs/java/util/HashMap.jml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/specs/java/util/HashMap.jml b/specs/java/util/HashMap.jml index 7de68c2b..2e48ee19 100644 --- a/specs/java/util/HashMap.jml +++ b/specs/java/util/HashMap.jml @@ -8,9 +8,9 @@ public class HashMap extends AbstractMap implements Map, Cloneabl public HashMap(); //@ public normal_behavior - //@ ensures this.theSize == m.theSize; - //@ ensures (\forall Object o; this.containsKey(k) <==> m.containsKey(k)); - //@ ensures (\forall Object o; m.containsKey(k); this.containsKey(k) && this.get(k) == m.get(k)); + //@ ensures this.size() == m.size(); + //@ ensures (\forall Object k; this.containsKey(k) <==> m.containsKey(k)); + //@ ensures (\forall Object k; m.containsKey(k); this.containsKey(k) && this.get(k) == m.get(k)); //@ pure public HashMap(Map m); From 3c4faa6d8655f97e99ecccf18e77c78f2dc845be Mon Sep 17 00:00:00 2001 From: Steven Lyubomirsky Date: Fri, 17 Aug 2018 15:27:19 -0700 Subject: [PATCH 05/10] Check for null in HashMap constructor --- specs/java/util/HashMap.jml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/specs/java/util/HashMap.jml b/specs/java/util/HashMap.jml index 2e48ee19..ce7ec703 100644 --- a/specs/java/util/HashMap.jml +++ b/specs/java/util/HashMap.jml @@ -8,9 +8,13 @@ public class HashMap extends AbstractMap implements Map, Cloneabl public HashMap(); //@ public normal_behavior + //@ requires m != null; //@ ensures this.size() == m.size(); //@ ensures (\forall Object k; this.containsKey(k) <==> m.containsKey(k)); //@ ensures (\forall Object k; m.containsKey(k); this.containsKey(k) && this.get(k) == m.get(k)); + //@ also public exceptional_behavior + //@ requires m == null; + //@ signals_only NullPointerException; //@ pure public HashMap(Map m); From eef15653b763fe4506d34c66f53ce0e1c9d2748b Mon Sep 17 00:00:00 2001 From: Steven Lyubomirsky Date: Fri, 17 Aug 2018 15:42:16 -0700 Subject: [PATCH 06/10] Avoid using quantifiers to specify HashMap constructor (catastrophic errors before) --- specs/java/util/HashMap.jml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/specs/java/util/HashMap.jml b/specs/java/util/HashMap.jml index ce7ec703..2aa502b7 100644 --- a/specs/java/util/HashMap.jml +++ b/specs/java/util/HashMap.jml @@ -10,8 +10,7 @@ public class HashMap extends AbstractMap implements Map, Cloneabl //@ public normal_behavior //@ requires m != null; //@ ensures this.size() == m.size(); - //@ ensures (\forall Object k; this.containsKey(k) <==> m.containsKey(k)); - //@ ensures (\forall Object k; m.containsKey(k); this.containsKey(k) && this.get(k) == m.get(k)); + //@ ensures this.entrySet().equals( m.entrySet() ); //@ also public exceptional_behavior //@ requires m == null; //@ signals_only NullPointerException; From 8952e2ccabbc886809ef3d0c1897d6e8f2fabf7a Mon Sep 17 00:00:00 2001 From: Steven Lyubomirsky Date: Wed, 22 Aug 2018 11:33:30 -0700 Subject: [PATCH 07/10] isImmutable is model field, keep it in -RAC blocks --- specs/java/util/ArrayList.jml | 2 +- specs/java/util/Collection.jml | 2 +- specs/java/util/Collections.jml | 14 +++++++------- specs/java/util/HashMap.jml | 2 +- specs/java/util/HashSet.jml | 2 +- specs/java/util/Map.jml | 28 +++++++++++++--------------- specs/java/util/Queue.jml | 2 +- specs/java/util/Vector.jml | 2 +- 8 files changed, 26 insertions(+), 28 deletions(-) diff --git a/specs/java/util/ArrayList.jml b/specs/java/util/ArrayList.jml index 2f884052..092b6aff 100644 --- a/specs/java/util/ArrayList.jml +++ b/specs/java/util/ArrayList.jml @@ -43,7 +43,7 @@ public class ArrayList extends AbstractList /*@ public model int capacity; in objectState; @*/ - //@ public invariant !isImmutable; + //-RAC@ public invariant !isImmutable; // METHODS AND CONSTRUCTORS //@ public normal_behavior diff --git a/specs/java/util/Collection.jml b/specs/java/util/Collection.jml index 104c726d..50f0c839 100644 --- a/specs/java/util/Collection.jml +++ b/specs/java/util/Collection.jml @@ -58,7 +58,7 @@ public interface Collection extends Iterable { * UnsupportedOperationException), required by various asImmutable*() * methods in Collections */ - //-RAC@ instance ghost public boolean isImmutable; in localState; + //-RAC@ model instance public boolean isImmutable; in localState; //+OPENJML@ immutable //@ pure diff --git a/specs/java/util/Collections.jml b/specs/java/util/Collections.jml index 4d0b035f..ca95ba53 100644 --- a/specs/java/util/Collections.jml +++ b/specs/java/util/Collections.jml @@ -50,7 +50,7 @@ public class Collections { //@ public normal_behavior //@ requires true; //@ ensures \fresh(\result); - //@ ensures \result.isImmutable; + //-RAC@ ensures \result.isImmutable; //@ ensures \result.content == c.content; // changes to original show //@ pure public static java.util.Collection unmodifiableCollection(java.util.Collection c); @@ -58,7 +58,7 @@ public class Collections { //@ public normal_behavior //@ requires true; //@ ensures \fresh(\result); - //@ ensures \result.isImmutable; + //-RAC@ ensures \result.isImmutable; //@ ensures \result.content == s.content; // changes to original show //@ pure public static java.util.Set unmodifiableSet(java.util.Set s); @@ -68,7 +68,7 @@ public class Collections { //@ public normal_behavior //@ requires true; //@ ensures \fresh(\result); - //@ ensures \result.isImmutable; + //-RAC@ ensures \result.isImmutable; //@ ensures \result.content == l.content; // changes to original show //@ pure public static java.util.List unmodifiableList(java.util.List l); @@ -76,7 +76,7 @@ public class Collections { //@ public normal_behavior //@ requires true; //@ ensures \fresh(\result); - //@ ensures \result.isImmutable; + //-RAC@ ensures \result.isImmutable; //@ ensures \result.content == m.content; // changes to original show //@ pure public static java.util.Map unmodifiableMap(java.util.Map m); @@ -109,7 +109,7 @@ public class Collections { //@ public normal_behavior //@ requires true; - //@ ensures \result.isImmutable; + //-RAC@ ensures \result.isImmutable; //@ ensures \result.isEmpty(); //@ // javadoc says it need not be fresh //@ pure @@ -119,7 +119,7 @@ public class Collections { //@ public normal_behavior //@ requires true; - //@ ensures \result.isImmutable; + //-RAC@ ensures \result.isImmutable; //@ ensures \result.isEmpty(); //@ // javadoc says it need not be fresh //@ pure @@ -127,7 +127,7 @@ public class Collections { //@ public normal_behavior //@ requires true; - //@ ensures \result.isImmutable; + //-RAC@ ensures \result.isImmutable; //@ ensures \result.isEmpty(); //@ // javadoc says it need not be fresh //@ pure diff --git a/specs/java/util/HashMap.jml b/specs/java/util/HashMap.jml index 2aa502b7..b7ec32e6 100644 --- a/specs/java/util/HashMap.jml +++ b/specs/java/util/HashMap.jml @@ -1,7 +1,7 @@ package java.util; public class HashMap extends AbstractMap implements Map, Cloneable, java.io.Serializable { - //@ public invariant !isImmutable; + //-RAC@ public invariant !isImmutable; //@ public normal_behavior //@ ensures initialAbstractMap(); diff --git a/specs/java/util/HashSet.jml b/specs/java/util/HashSet.jml index 98b7f45b..f5474eea 100644 --- a/specs/java/util/HashSet.jml +++ b/specs/java/util/HashSet.jml @@ -2,7 +2,7 @@ package java.util; public class HashSet extends AbstractCollection implements Set, Cloneable, java.io.Serializable { - //@ public invariant !isImmutable; + //-RAC@ public invariant !isImmutable; //@ public normal_behavior ensures true; //@ pure diff --git a/specs/java/util/Map.jml b/specs/java/util/Map.jml index 4a32d29b..d3191f28 100644 --- a/specs/java/util/Map.jml +++ b/specs/java/util/Map.jml @@ -155,7 +155,7 @@ public interface Map { * UnsupportedOperationException), required by various asImmutable*() * methods in Collections */ - //-RAC@ public instance ghost boolean isImmutable; + //-RAC@ model public instance boolean isImmutable; //@ public normal_behavior //@ ensures (* \result == content.theSize *); @@ -281,14 +281,14 @@ public interface Map { @ signals (NullPointerException) key == null @ && (* if this map doesn't support null keys *); @*/ - /*@ also public exceptional_behavior + /*-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; @@ -344,20 +344,18 @@ public interface Map { //@ ensures \result == _keySet; /*@ pure @*/ Set keySet(); - /*@ public normal_behavior - @ ensures \result != null; - @ ensures \result.size() >= 0; // FIXME - why needed? - @ ensures isImmutable <==> \result.isImmutable; - // FIXME - @*/ + //@ public normal_behavior + //@ ensures \result != null; + //@ ensures \result.size() >= 0; // FIXME - why needed? + //-RAC@ ensures isImmutable <==> \result.isImmutable; + //@ // FIXME /*@ pure @*/ Collection values(); - /*@ public normal_behavior - @ ensures \result != null; - @ ensures \result.size() >= 0; // FIXME - why needed? - @ ensures isImmutable <==> \result.isImmutable; - // FIXME - @*/ + //@ public normal_behavior + //@ ensures \result != null; + //@ ensures \result.size() >= 0; // FIXME - why needed? + //-RAC@ ensures isImmutable <==> \result.isImmutable; + //@ // FIXME /*@ pure @*/ Set> entrySet(); /*@ diff --git a/specs/java/util/Queue.jml b/specs/java/util/Queue.jml index 7dc0b769..2abbbae2 100644 --- a/specs/java/util/Queue.jml +++ b/specs/java/util/Queue.jml @@ -28,7 +28,7 @@ package java.util; public interface Queue extends Collection { - //@ public invariant !isImmutable; + //-RAC@ public invariant !isImmutable; /*-RAC@ public normal_behavior @ requires n >= 0 && n < content.theSize; diff --git a/specs/java/util/Vector.jml b/specs/java/util/Vector.jml index c45edd8f..f4b226a7 100644 --- a/specs/java/util/Vector.jml +++ b/specs/java/util/Vector.jml @@ -55,7 +55,7 @@ public class Vector extends AbstractList protected /*@ spec_public @*/ int elementCount; //@ in objectState; - //@ public invariant !isImmutable; + //-RAC@ public invariant !isImmutable; //@ public invariant 0 <= elementCount; // I'm commenting out the following, since this is guaranteed by the postcondition of size() From 5b18e8c29fedd5e83ad808fe45f5fc138399b885 Mon Sep 17 00:00:00 2001 From: Steven Lyubomirsky Date: Tue, 28 Aug 2018 18:18:20 -0700 Subject: [PATCH 08/10] Fix merge conflict by switching tabs to spaces in HashSet.jml --- specs/java/util/HashSet.jml | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/specs/java/util/HashSet.jml b/specs/java/util/HashSet.jml index f5474eea..f501fab5 100644 --- a/specs/java/util/HashSet.jml +++ b/specs/java/util/HashSet.jml @@ -7,35 +7,35 @@ public class HashSet extends AbstractCollection implements Set, Cloneab //@ public normal_behavior ensures true; //@ pure public HashSet(); - + //@ public normal_behavior ensures true; //@ pure public HashSet(Collection c); - + //@ public normal_behavior ensures true; //@ pure public HashSet(int initialCapacity); - + //@ public normal_behavior ensures true; //@ pure public HashSet(int initialCapacity, float loadFactor); - + public boolean add(E e); - + public void clear(); - + public Object clone(); - + public boolean contains(Object o); - + //@ also public normal_behavior ensures true; //@ pure public boolean isEmpty(); - + public Iterator iterator(); - + public boolean remove(Object o); - + //@ also public normal_behavior ensures true; //@ pure public int size(); From b23d3c5a4e29fdb829bd83e91064dff1d3b3b08c Mon Sep 17 00:00:00 2001 From: Steven Lyubomirsky Date: Thu, 6 Sep 2018 15:42:32 -0700 Subject: [PATCH 09/10] Remove invariants about isImmutable, assert in constructors & methods (inheriting classes may be immutable) --- specs/java/util/ArrayList.jml | 7 ++++--- specs/java/util/HashMap.jml | 4 ++-- specs/java/util/HashSet.jml | 6 ++++-- specs/java/util/Queue.jml | 5 +++-- specs/java/util/Vector.jml | 7 ++++++- 5 files changed, 19 insertions(+), 10 deletions(-) diff --git a/specs/java/util/ArrayList.jml b/specs/java/util/ArrayList.jml index 092b6aff..ee17fc9a 100644 --- a/specs/java/util/ArrayList.jml +++ b/specs/java/util/ArrayList.jml @@ -33,6 +33,7 @@ public class ArrayList extends AbstractList @ initialAbstractList() && @ capacity == initialCapacity && @ isEmpty() && + @ !isImmutable && @ containsNull; @ public pure model boolean initialArrayList(int initialCapacity); @*/ @@ -43,8 +44,6 @@ public class ArrayList extends AbstractList /*@ public model int capacity; in objectState; @*/ - //-RAC@ public invariant !isImmutable; - // METHODS AND CONSTRUCTORS //@ public normal_behavior //@ requires 0 <= initialCapacity; @@ -70,6 +69,7 @@ public class ArrayList extends AbstractList @ 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; @@ -81,7 +81,7 @@ public class ArrayList extends AbstractList /*-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(); @@ -91,6 +91,7 @@ public class ArrayList extends AbstractList @ 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/HashMap.jml b/specs/java/util/HashMap.jml index b7ec32e6..d50021cf 100644 --- a/specs/java/util/HashMap.jml +++ b/specs/java/util/HashMap.jml @@ -1,16 +1,16 @@ package java.util; public class HashMap extends AbstractMap implements Map, Cloneable, java.io.Serializable { - //-RAC@ public invariant !isImmutable; - //@ 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; diff --git a/specs/java/util/HashSet.jml b/specs/java/util/HashSet.jml index f501fab5..5d44921a 100644 --- a/specs/java/util/HashSet.jml +++ b/specs/java/util/HashSet.jml @@ -2,21 +2,23 @@ package java.util; public class HashSet extends AbstractCollection implements Set, Cloneable, java.io.Serializable { - //-RAC@ public invariant !isImmutable; - //@ public normal_behavior ensures true; + //-RAC@ ensures !isImmutable; //@ pure public HashSet(); //@ public normal_behavior ensures true; + //-RAC@ ensures !isImmutable; //@ pure public HashSet(Collection 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); diff --git a/specs/java/util/Queue.jml b/specs/java/util/Queue.jml index 2abbbae2..3854403a 100644 --- a/specs/java/util/Queue.jml +++ b/specs/java/util/Queue.jml @@ -28,8 +28,6 @@ package java.util; public interface Queue extends Collection { - //-RAC@ public invariant !isImmutable; - /*-RAC@ public normal_behavior @ requires n >= 0 && n < content.theSize; @ ensures !\fresh(\result); @@ -47,6 +45,7 @@ public interface Queue extends Collection { @*/ /*-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; @@ -98,6 +97,7 @@ public interface Queue extends Collection { @ 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))); @@ -112,6 +112,7 @@ public interface Queue extends Collection { @ 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/Vector.jml b/specs/java/util/Vector.jml index f4b226a7..afdc3115 100644 --- a/specs/java/util/Vector.jml +++ b/specs/java/util/Vector.jml @@ -55,7 +55,6 @@ public class Vector extends AbstractList protected /*@ spec_public @*/ int elementCount; //@ in objectState; - //-RAC@ public invariant !isImmutable; //@ public invariant 0 <= elementCount; // I'm commenting out the following, since this is guaranteed by the postcondition of size() @@ -72,6 +71,7 @@ public class Vector extends AbstractList @ ensures containsNull; @ ensures isEmpty(); @ ensures elementCount == 0; + @ ensures !isImmutable; @*/ public /*@ pure @*/ Vector (int initialCapacity, int capacityIncrement); @@ -82,6 +82,7 @@ public class Vector extends AbstractList @ ensures containsNull; @ ensures isEmpty(); @ ensures elementCount == 0; + @ ensures !isImmutable; @*/ public /*@ pure @*/ Vector(int initialCapacity); @@ -96,6 +97,7 @@ public class Vector extends AbstractList /*@ public normal_behavior @ requires c != null; + @ ensures !isImmutable; @ ensures elementCount == c.size(); @ ensures this.containsNull == c.containsNull; @ ensures this.content.theSize == c.content.theSize; @@ -121,6 +123,7 @@ public class Vector extends AbstractList // 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 extends AbstractList //@ 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 @@ -164,6 +168,7 @@ public class Vector extends AbstractList @ ensures elementCount == newSize; */ /*-RAC@ ensures \not_modified(theString,theHashCode); @ ensures \not_modified(containsNull); + @ ensures \not_modified(isImmutable); @ ensures (\forall int i; 0<=i && i Date: Thu, 6 Sep 2018 15:46:01 -0700 Subject: [PATCH 10/10] Update content owner invariant to mention immutability --- specs/java/util/Collection.jml | 2 +- specs/java/util/Map.jml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/specs/java/util/Collection.jml b/specs/java/util/Collection.jml index 50f0c839..babb0883 100644 --- a/specs/java/util/Collection.jml +++ b/specs/java/util/Collection.jml @@ -73,7 +73,7 @@ public interface Collection extends Iterable { @*/ //-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 diff --git a/specs/java/util/Map.jml b/specs/java/util/Map.jml index d3191f28..ecb68176 100644 --- a/specs/java/util/Map.jml +++ b/specs/java/util/Map.jml @@ -77,7 +77,7 @@ public interface Map { */ //-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 <==> (