LinkedHashMap + LinkedHashSet models: insertion/access order over HashMap/HashSet - #46
Draft
tautschnig wants to merge 3 commits into
Draft
LinkedHashMap + LinkedHashSet models: insertion/access order over HashMap/HashSet#46tautschnig wants to merge 3 commits into
tautschnig wants to merge 3 commits into
Conversation
…eneric-element annotation Three top-level org.cprover support classes for collection models' iterator()/enhanced-for support. They are inert until collection models reference them (none in this repo do yet -- the javadoc describes intended usage); landing them separately keeps the model changes reviewable. - CProverArrayLikeIterator<E>: generic snapshot iterator over an Object[]-backed collection; captures (storage, size) at iterator() time. Top-level rather than an inner class deliberately: a non-static inner class's implicit this$0 creates a Collection <-> Iterator lazy-class-loading cycle that aborts JBMC's nondet initialisation of abstract collection parameters. The class javadoc carries the full design rationale (snapshot-vs-fail-fast trade-off, iteration-order conformance, and the documented opt-in future paths for CME modelling and Iterator.remove()). next() past the end throws NoSuchElementException per the JDK contract. An assume() guard on the precondition would be unsound here: it would prune exactly the executions in which target code over-iterates, hiding those bugs behind vacuously-passing paths; modelling the throw keeps them observable with the correct exception type. - CProverMapEntry<K, V>: read-only snapshot Map.Entry for entrySet() views of parallel-array map models. Deliberately final; entry-driven mutation calls for a separate write-through entry class (documented), not subclassing. - @CProverGenericArrayElement: marks an Object[] field as holding a model class's generic-parameter elements, so JBMC's nondet object factory can specialise the element type. Co-authored-by: Kiro <[email protected]>
Executable model of java.util.HashSet over a duplicate-free Object[] prefix: add/remove/contains/size/isEmpty/clear, addAll/removeAll/ retainAll/containsAll, toArray, and iterator() via CProverArrayLikeIterator (snapshot semantics). Iteration is storage order, conformant with HashSet's unspecified-order contract. Null elements are supported per the JDK. A package-private wrapping constructor exposes a pre-existing storage prefix so map models can build keySet()/entrySet() views without copying. Co-authored-by: Kiro <[email protected]>
…hMap/HashSet LinkedHashMap is an ORDER OVERLAY over the HashMap model: the key-value association lives in the superclass, while a parallel key list maintains the SPECIFIED iteration order -- insertion order, or access order with the (capacity, loadFactor, accessOrder) constructor, where get/getOrDefault and put-of-existing-key move the key to the end per the JDK. put/remove/ clear/putIfAbsent keep the overlay in sync (putAll delegates to put in the HashMap model, so bulk insertion is ordered too); keySet()/values()/ entrySet() are rebuilt from the ordered key list (snapshot views). removeEldestEntry is consulted after each insertion per the JDK contract, so LRU-cache subclasses verify correctly. Methods that would mutate the map behind the overlay (compute/computeIfAbsent/computeIfPresent/merge) are notModelled rather than silently inherited with a stale order. LinkedHashSet is behaviourally the HashSet model (whose Object[]-prefix storage is already insertion-ordered: add appends, remove shifts left); the subclass provides the JDK type identity and constructors. Co-authored-by: Kiro <[email protected]>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Depends-on: #45
LinkedHashMap is an ORDER OVERLAY over the HashMap model: the key-value
association lives in the superclass, while a parallel key list maintains
the SPECIFIED iteration order -- insertion order, or access order with the
(capacity, loadFactor, accessOrder) constructor, where get/getOrDefault
and put-of-existing-key move the key to the end per the JDK. put/remove/
clear/putIfAbsent keep the overlay in sync (putAll delegates to put in the
HashMap model, so bulk insertion is ordered too); keySet()/values()/
entrySet() are rebuilt from the ordered key list (snapshot views).
removeEldestEntry is consulted after each insertion per the JDK contract,
so LRU-cache subclasses verify correctly. Methods that would mutate the
map behind the overlay (compute/computeIfAbsent/computeIfPresent/merge)
are notModelled rather than silently inherited with a stale order.
LinkedHashSet is behaviourally the HashSet model (whose Object[]-prefix
storage is already insertion-ordered: add appends, remove shifts left);
the subclass provides the JDK type identity and constructors.
Co-authored-by: Kiro [email protected]