HashSet model: deterministic Object[]-backed set - #45
Draft
tautschnig wants to merge 2 commits into
Draft
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 <kiro-agent@users.noreply.github.com>
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 <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
model-hashset
branch
from
July 29, 2026 00:59
29791f2 to
ed2267b
Compare
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: #42 (first commit in this PR)
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 kiro-agent@users.noreply.github.com