Update Semantics
Spec collections (Map, Set, Seq, Multiset) are ghost value models in verification. Operations such as Map.update, Set.union, Seq.concat, and Multiset.minus return new values and do not consume the old version. Aliasing is allowed.
Threading Updates
Threading is the practice of chaining updates through sequential variable bindings. It is optional, but still a clear way to show the evolution of a collection value in specs.
old() Collections
Referring to previous collection state in postconditions.
Element Type Restrictions
Spec collections (Map, Set, Seq, Multiset) only accept spec-immutable key, value, and element types in verification mode, except opaque/token handles by identity. This page explains what types are allowed, what types are rejected, and why.