Once we have a sequence, we can query different properties of that sequence. The syntax `s5[i]` can be used to retrieve the element at index `i` from sequence `s5`. The notation `s5.head` is shorthand for `s5[0]`. The length of a sequence `s5` can be obtained by using the notation `|s5|`. Two sequences can be compared using the `==` operator where they are equal iff they are of the same length and the elements at the same indices are equal. ```pvl seq

## Constructing sequences from existing sequences As mentioned above sequences are immutable, however it is possible to construct a new sequence from an existing sequence. Elements can be added to a sequence in two ways. The first way is by concatenating two sequences `s6 + s7`. This expression represents a new sequence with the elements of `s6` followed by the elements of `s7`. The second way is to add a single value to the front of a sequence. The syntax `e::s6` is used to prepend `e` at the front of `s6`. ```pvl seq

Constructs a sequence with elements of type `T` initiliazed with values `e1`, `e2`, etc. When the sequence is not initialized, an empty sequence is constructed. Constructor | `seq

Constructs a sequence with elements of type `T` initiliazed with values `e1`, `e2`, etc. This syntax requires the sequence to be initialized. Constructor | `seq

Constructs an empty sequence with element of type `T` Length | `int` | `\|s1\|` or `s1.size`

Returns the length/cardinality of the sequence `s1` Empty | `boolean` | `s1.isEmpty`

Returns whether `|s1| == 0` Comparison | `boolean` | `s1 == s2`

Returns `true` if `s1` and `s2` are equivalent Concatenation | `seq

Denotes the sequence with elements from `s1` followed by the elements of `s2` Contains | `boolean` | `e \in xs` or `xs.contains(e)`. True if `e` is in `xs`. Indexing | `T` | `s1[i]`

Returns the element at index `i` of sequence `s1` Head | `T` | `s1.head`

Returns the first element of sequence `s1` Tail | `seq

Denotes the sequence with the elements from `s1` excluding the first element Prepend | `seq

Denotes the sequence with elements of `xs` prepended with the element `x` Slicing | `seq

Denotes the subsequence of sequence `s1` from index `i` until index `j` (exclusive) Dropping | `seq

Denotes the subsequence starting at `i` Taking | `seq`

Denotes the subsequence of the first `j` elements Updating | `seq

Denotes the sequence with elements from `s1` where index `i` has been updated to value `v` Removing | `seq`

Denotes the sequence where the element at index `i` is removed. Equivalent to `s1[..i] + s1[i+1..]` Summation | int | `(\sum int i; low <=i && i< up; s1[i]);`

Sum the elements of a sequence of integers `s1` between the indices `low` and `up` (exclusive) ## Set Short Description | Return type | Syntax ----------------- | ------------- | ------------- Constructor | `set

Constructs a set with elements of type `T` initiliazed with values `e1`, `e2`, etc. When the set is not initialized, an empty set is constructed. Constructor | `set

Constructs a set with elements of type `T` initiliazed with values `e1`, `e2`, etc. This syntax requires the set to be initiliazed. Constructor | `set

Constructs an empty set with element of type `T` Length | `int` | `\|s1\|` or `s1.size`

Returns the length/cardinality of the set `s1` Empty | `boolean` | `s1.isEmpty`

Returns whether `|s1| == 0` Comparison | `boolean` | `s1 == s2`

Returns `true` if `s1` and `s2` are equivalent Membership | `boolean` | `e \in s1` or `s1.contains(e)`

Returns `true` if the value `e` is in the set `s1` Set Union | `set

Denotes the set of all elements from sets `s1` and `s2` of the same type `T` Set Difference | `set

Denotes the set of all elements from set `s1` that are not in set `s2` Subset | `boolean` | `s1 <= s2` or `s1.subsetOf(s2)`

Returns `true` if set `s1` is a subset of set `s2` Strict Subset | `boolean` | `s1 < s2` or `s1.strictSubsetOf(s2)`

Returns `true` if set `s1` is a strict subset of set `s2` Intersection |`set

Denotes the set of all elements that are both in sets `s1` and `s2` Set Comprehension | `set

Constructs a set of elements of the form `main` over the quantified variables in `variables` that match `selector` ## Bag Short Description | Return type | Syntax ----------------- | ----------- | ------------- Constructor | `bag

Constructs a bag with elements of type `T` initiliazed with values `e1`, `e2`, etc. When the bag is not initialized, an empty bag is constructed. Constructor | `bag

Constructs a bag with elements of type `T` initiliazed with values `e1`, `e2`, etc. This syntax requires the bag to be initiliazed. Constructor | `bag

Constructs an empty bag with element of type `T` Length | `int` | `\|b1\|` or `b1.size`

Returns the length/cardinality of the bag `b1` Empty | `boolean` | `b1.isEmpty`

Returns whether `|b1| == 0` Multiplicity | `int` | `e \in b1` or `b1.count(e)`

Returns the number of occurrences of value `e` in bag `b1` Comparison | `boolean` | `b1 == b2`

Returns `true` if `b1` and `b2` are equivalent Bag Union | `bag

Denotes the bag of all elements from bags `b1` and `b2` of the same type `T` Bag Difference | `bag

Denotes the bag of all elements from bag `b1` that are not in bag `b2` Subset | `boolean` | `b1 <= b2` or `b1.subbagOf(b2)`

Returns `true` if bag `b1` is a subset of bag `b2` Strict Subset | `boolean` | `b1 < b2` or `b1.strictSubbagOf(b2)`

Returns `true` if bag `b1` is a strict subset of bag `b2` Intersection |`bag

Denotes the bag of all elements that are both in bags `b1` and `b2` ## Map Short Description | Return type | Syntax ----------------- | ----------- | ------------- Constructor | `map

Constructs a map with key-value pairs of type `K` and `V` respectively initiliazed with pairs `k1,v1`, `k2,v2`, etc. Build/Add | `map

Adds the key/value pair `(k1,v1)` to the map `m1`. If the key is already present in `m1`, update the value of the key. GetByKey | `V` | `m1.get(k1)` or `map[k1]`

Gets the value mapped by the key `k1` from the map `m1`. Remove | `map

Removes the key `k1` and its associated value from the map `m1`. Length | `int` | `m1.size` or `\|m1\|`

Returns the length/cardinality of the map `m1` Empty | `boolean` | `m1.isEmpty`

Returns whether `|m1| == 0` Comparison | `boolean` | `m1.equals(m2)` or `m1 == m2`

Returns `true` if the keysets of `m1` and `m2` are equivalent and the keys map to the same values. Key Set | `set

Returns a set of keys in map `m1` Value Set | `set

Returns a set of the values in map `m1` Item Set | `set

Returns a set of tuples corresponding to the key-value pairs in map `m1` Disjoint | `boolean` | `m1.disjoint(m2)`

Returns `true` if no key is in both the key set of `m1` and the key set of `m2`. ## Tuple Short Description | Return type | Syntax ----------------- | ----------- | ------------- Constructor | `tuple

Construct a tuple with first element `fst` (of type `F`) and second element `snd` (of type `S`) Get First Element | `F` | `t.fst`

Get the first element of the tuple `t` (of type `tuple

Get the second element of the tuple `t` (of type `tuple

Constructs an option which contains the element `e` of type `T` Constructor | `option

Returns the option `None` Getter | `T` | `e.get`

Returns the value contained in the option if it is filled Getter | `T` | `e.getOrElse(t)`

Returns the value contained in the option, `t` otherwise Comparison | `boolean` | `o1 == o2`

Returns `true` if the element contained in the option `o1` is equivalent to the element wrapped in the option `o2`, or both are empty # Custom ADTs ADTs can be useful to provide VerCors with domain-specific assumptions. For example, a custom int-tuple ADT can be defined in PVL as follows: ```java adt MyTuple { pure MyTuple cons(int l, int r); pure int left(MyTuple t); pure int right(MyTuple t); axiom (\forall int l, int r; left(cons(l, r)) == l); axiom (\forall int l, int r; right(cons(l, r)) == r); axiom (\forall int l1, int l2, int r1, int r2; (cons(l1, r1) == cons(l2, r2)) ==> (l1 == l2 && r1 == r2)); } void testTuple(MyTuple t) { assert MyTuple.cons(1, 2) == MyTuple.cons(1, 2); assert MyTuple.cons(1, 2) != MyTuple.cons(3, 4); } ``` Note however that it is easy to make mistakes and define axioms from which false can be derived. If this happens, and your custom ADT is used in your code or contracts, from that point on VerCors assumes false, which makes every proof obligation after that point trivial to prove. Furthermore, when writing quantifiers in ADTs it is important to also define triggers. VerCors and its backend can often infer some trigger, but these are usually suboptimal. Custom ADTs are supported in all frontends.