From 8b5d31f746589068b683910e856c58482940316e Mon Sep 17 00:00:00 2001 From: Steven Lyubomirsky Date: Mon, 27 Aug 2018 11:28:42 -0700 Subject: [PATCH 1/2] Have specialized specification for making an ArrayList from a List --- specs/java/util/ArrayList.jml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/specs/java/util/ArrayList.jml b/specs/java/util/ArrayList.jml index 79698ae4..225c5cb1 100644 --- a/specs/java/util/ArrayList.jml +++ b/specs/java/util/ArrayList.jml @@ -68,6 +68,15 @@ public class ArrayList extends AbstractList @ this.get(i) == (c.iterator().nthNextElement(i))); @ ensures capacity == c.size()*1.1; @ ensures containsNull == c.containsNull; + @ {| + @ requires !(c instanceof List); + @ ensures (\forall int i; 0 <= i && i < c.size(); + @ this.get(i) == (c.iterator().nthNextElement(i))); + @ also + @ requires c instanceof List; + @ ensures (\forall int i; 0 <= i && i < c.size(); + @ this.get(i) == ((List) c).get(i)); + @ |} @ also @ public exceptional_behavior @ requires c == null; From e661a0044a9da6c9f96c52275279f79a90d28270 Mon Sep 17 00:00:00 2001 From: Steven Lyubomirsky Date: Mon, 27 Aug 2018 12:34:39 -0700 Subject: [PATCH 2/2] Remove old nthIterator ensures clause from ArrayList constructor --- specs/java/util/ArrayList.jml | 2 -- 1 file changed, 2 deletions(-) diff --git a/specs/java/util/ArrayList.jml b/specs/java/util/ArrayList.jml index 225c5cb1..98921582 100644 --- a/specs/java/util/ArrayList.jml +++ b/specs/java/util/ArrayList.jml @@ -64,8 +64,6 @@ public class ArrayList extends AbstractList @ requires c != null; @ requires c.size() <= (Integer.MAX_VALUE/11)*10; @ ensures this.size() == c.size(); - @ ensures (\forall int i; 0 <= i && i < c.size(); - @ this.get(i) == (c.iterator().nthNextElement(i))); @ ensures capacity == c.size()*1.1; @ ensures containsNull == c.containsNull; @ {|