*This section discusses axiomatic data types supported by VerCors.* Axiomatic data types are data types that are defined by a set of uninterpreted functions and axioms that define the behavior of these functions. This is in contrast to concrete data types which are defined by their implementation in a programming language such as Java or C++. Axiomatic datatypes are not to be confused with _algebraic_ datatypes. In the sections below, we are going to go over all ADTs supported by VerCors, give the definition of each, and show examples of common operations defined on them. A reference table can be found at the end showing all the operations defined on the ADTs. The axiomatizations used by VerCors and its back end Viper can be found [here](https://github.com/viperproject/silicon/tree/master/src/main/resources/dafny_axioms) (for sequences sets and bags) and [here](https://github.com/utwente-fmt/vercors/tree/dev/src/main/universal/res/adt) (for the other ADTs). Finally, it is also possible to create custom ADTs, though with limited syntax support. This is discussed at the end of this section. # Sequence Sequences are an ordered/enumerated collection also commonly referred to as lists. Sequences are finite and immutable (i.e. once created they cannot be altered). There are two ways to construct a sequence: the explicit syntax and the implicit syntax. The explicit syntax requires the type of the sequence to be explicitly defined. For example, s1 is a sequence of integers initialized with the values 1, 2 and 3 and s2 is an empty sequence of integers. pvl seq s1 = seq { 1, 2, 3 }; seq s2 = seq { };  The implicit syntax is a shorter syntax. If the sequence is initialized with at least one value (using the implicit syntax), VerCors infers the type of the sequence. An empty sequence can be constructed by providing the type of the sequence. For example, s3 is equivalent to s1 and s4 is equivalent to s2. Notice how there is no space between [ and t, this is mandated by the VerCors grammar. pvl seq s3 = [ 1, 2, 3 ]; seq s4 = [t: int ]; 
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 s5 = [ 1, 2, 4, 8, 16 ]; assert s5[3] == 8; assert |s5| == 5; assert s5 == seq { 1, 2, 4, 8, 16 }; 
## 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 s6 = [ 1, 2, 4, 8, 16 ]; assert 0::s6 == [ 0, 1, 2, 4, 8, 16 ]; seq s7 = [ 32, 64, 128 ]; assert s6 + s7 == [ 1, 2, 4, 8, 16, 32, 64, 128 ];  It is also possible to take a subsequence from an existing sequence. The syntax s8[i..j] is used to take the elements from s8 from index i to index j (exclusive). By omitting either the lower bound or upper bound, one can take or drop from a sequence. The notation s8.tail can be used as a shorthand for s8[1..]. pvl seq s8 = [ 1, 2, 4, 8, 16 ]; assert s8[1..4] == [ 2, 4, 8 ]; assert s8[..2] == [ 1, 2 ]; assert s8.tail == s8[1..];  ## Examples ### Sortedness Sortedness is a property that is often used in the verification of sorting algorithms. The sortedness property for a sequence of integers could be defined as follows: pvl pure boolean sorted(seq xs) = (\forall int i ; 0 <= i && i < |xs|-1; xs[i] <= xs[i+1]);  ### Distinct Element Another property on sequences is the uniqueness of the elements. This property could be expressed for a sequence of integers as follows: pvl pure boolean distinct(seq s) = (\forall int i; 0 <= i && i < s.length; (\forall int j; 0 <= j && j < s.length && s[i] == s[j]; i == j) );  ### Maximum element Recursive functions are often used to transform or reduce a sequence. The example below goes over a sequence to get its maximum value. This function could be defined for a sequence of integers as follows: pvl requires |xs| > 0; ensures (\forall int i; 0 <= i && i < |xs|; xs[i] <= \result); pure static int max(seq xs) = 1 == |xs| ? xs[0]: (xs[0] > max(xs[1..]) ? xs[0]: max(xs[1..] ) );  # Set Sets are an unordered collection with unique values. Sets are finite and immutable (i.e. once created they cannot be altered). Similar to sequences, there are two ways to construct a set: the explicit syntax and the implicit syntax. The explicit syntax requires the type of the set explicitly defined. For example, s1 is a set of integers initialized with the values 1, 2 and 3 and s2 is an empty set of integers. pvl set s1 = set { 1, 2, 3, 2 }; set s2 = set { };  The implicit syntax is a shorter syntax. If the set is initialized with at least one value (using the implicit syntax), VerCors infers the type of the set. An empty set can be constructed by providing the type of the set. For example, s3 is equivalent to s1 and s4 is equivalent to s2. Notice how there is no space between { and t, this is mandated by the VerCors grammar. pvl set s3 = { 1, 2, 2, 3 }; set s4 = {t: int };  Once we have a set, we can query different properties of that set. The length of a set s5 can be obtained by using the notation |s5|. Two set s6 and s7 can be compared using the == operator where they are equal iff all elements of s6 are in s7 and all elements of s7 are in s6. The syntax e1 \in s8 is used to check if set s8 contains the element e1. The < and <= operators denote the strict subset and subset operators respectively. pvl set s5 = { 1, 2, 2, 3 }; set s6 = { 3, 4, 5, 6 }; set s7 = { 1, 2 }; set s8 = { 2, 3 }; int e1 = 3; assert |s5| == 3; assert s6 != s7; assert e1 \in s8; assert s8 < s5;  ## Constructing sets from existing sets As mentioned above sets are immutable, however it is possible to construct a new set from an existing set. There are several operations defined on sets that are part of set theory. The union of two sets is denoted by s5 + s6, the difference between two sets is denoted by s5 - s6 and the intersection of two sets is denoted by s5 * s6. pvl set s5 = { 1, 2, 2, 3 }; set s6 = { 3, 4, 5, 6 }; assert s5 + s6 == { 1, 2, 3, 4, 5, 6 }; assert s5 - s6 == { 1, 2 }; assert s6 - s5 == { 4, 5, 6}; assert s5 * s6 == { 3 };  ## Set comprehension An advanced way to create a set is using *set comprehension*. The syntax is set { main | variables; selector } and consists of three parts: the main, the variables and the selector. The variables are the variables that are quantified over and these variables can be bound or unbound. From the quantified variables, we can select specific values by using the selector expression. This is a Boolean expression that selects (a part of) the quantified variables. With the selected set of variables to quantify over, we express the value that is going to be part of the resulting set using the main expression. For example, we can construct the set of all even integers from 0 to 9 as follows:  set {x | int x <- {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}; x % 2 == 0};  To use more complex main expressions (i.e. non-identity functions), it is recommended to wrap the expression in a function and use that function in the main expression. For example, suppose we have a set of integers from 0 to 5 (inclusive) and we want to construct the set of integers where each element is doubled, we could use set comprehension as follows: pvl class SetComp { requires 0 <= j && j < 5; void myMethod(int j) { set a = set {SetComp.plus(x, x) | int x; x >= 0 && x <= 5 }; assert plus(1, 1) in a; assert plus(j, j) in a; } pure static int plus(int a, int b) = a+b; }  Here we define a function plus to wrap the expression a+b and use an invokation of the plus function as the main of our set comprehension. # Bag A bag (also called a multiset) is an unordered collection. They are equivalent to sequences without order, or sets with duplicates. Bags are finite and immutable (i.e. once created they cannot be altered). Similar to sequences and sets, there are two ways to construct a bag: the explicit syntax and the implicit syntax. The explicit syntax requires the type of the bag explicitly defined. For example, b1 is a bag of integers initialized with the values 1, 2, 2 and 3 and b2 is an empty bag of integers. pvl bag b1 = bag { 1, 2, 3, 2 }; bag b2 = bag { };  The implicit syntax is a shorter syntax. If the bag is initialized with at least one value (using the implicit syntax), VerCors infers the type of the bag. An empty bag can be constructed by providing the type of the bag. For example, b3 is equivalent to b1 and b4 is equivalent to b2. Notice how there is no space between b{ and t, this is mandated by the VerCors grammar. pvl bag b3 = b{ 1, 2, 2, 3 }; bag b4 = b{t: int };  Once we have a bag, we can query different properties of that bag. The length of a bag b5 can be obtained by using the notation |b5|. The syntax e1 \in b6 is used to get the multiplicity (or number of occurrences) of an element e1 in the bag b6. Two bags b7 and b8 can be compared using the == operator where they are equal iff for all elements e2, the multiplicity of e2 in b7 and b8 are equal. The < and <= operators denote the strict subset and subset operators respectively. pvl bag b5 = b{ 1, 2, 2, 3 }; bag b6 = b{ 3, 4, 5, 6, 5 }; bag b7 = b{ 1, 2, 3, 2, 2, 6 }; bag b8 = b{ 6, 1, 2, 2, 2, 3 }; int e1 = 5; assert |b5| == 4; assert (e1 \in b6) == 2; assert b5 <= b7 && b5 < b8; assert b7 == b8;  ## Constructing bags from existing bags As mentioned above bags are immutable, however it is possible to construct a new bag from an existing bag. The union of two bags is denoted by b9 + b10, the difference between two bags is denoted by b11 - b12 and the intersection of two bags is denoted by b13 * b14. pvl bag b9 = bag { 3 }; bag b10 = bag { 3, 4 }; bag b11 = bag { 1, 2, 2, 3 }; bag b12 = bag { 2, 3, 3, 4 }; bag b13 = bag { 1, 1, 2, 3 }; bag b14 = bag { 2, 3, 3, 4 }; assert b9 + b10 == bag { 3, 3, 4 }; assert b12 - b11 == bag { 3, 4 }; assert b11 - b12 == bag { 1, 2 }; assert b13 * b14 == bag { 2, 3 };  ## Examples TODO # Map Maps are an unordered, collection of key/value pairs with unique keys. Maps are finite and immutable (i.e. once created they cannot be altered). A map can be constructed using the syntax map { k1 -> v1, k2 -> v2, ...}. This syntax constructs a map with keys/value pairs (k1, v1) and (k2, v2) (of type K and type V respectively). An empty map can be constructed by declaring no key/value pair. pvl map m1 = map{1 -> true, 2 -> true, 0 -> false}; map m2 = map{1 -> true, 2 -> true, 0 -> false, 1 -> false, 1 -> true}; assert m1 == m2;  Once we have a map, we can query different properties of that map. Given a key k1, we can get its associated value in map m1 using the syntax m1[k1] or m1.get(k1). The cardinality/size of the map can be queried using the syntax |m1| or m1.size. The size of a map is equivalent to the size of its key set. The key, value and key/value pair sets can be obtained using the notations m1.keys, m1.values and m1.items respectively. pvl map m1 = map{1 -> true, 2 -> true, 0 -> false}; assert |m1| == 3; assert m1[0] == false; assert m1[1] == true; assert m1[2] == true; assert m1.keys == { 1, 2, 0 }; assert m1.values == { true, false }; assert tuple { 0, false } \in m1.items; assert tuple { 1, true } \in m1.items; assert tuple { 2, true } \in m1.items;  We can add a key/value pair (k4, v4) to the map m4 using the syntax m4.add(k4, v4). If the key was already present in m4, its value gets updated. We can also remove a key k5 from a map m5 using the function m5.remove(k5). pvl map m1 = map{}; map m2 = m1.add(1, 1).add(2, 4).add(3, 9); map m3 = m2.remove(2); map m4 = m3.remove(3).remove(1); assert |m1| == 0; assert m2[1] == 1; assert m2[2] == 4; assert m2[3] == 9; assert !(2 \in m3.keys); assert m3[1] == 1; assert m3[3] == 9; assert |m4| == 0;  ## Examples TODO # Tuple A tuple is an ordered, immutable collection containing exactly two elements. A tuple can be constructed using the syntax tuple { fst, snd }. This syntax constructs a tuple with the first value fst of type F and the second value snd of type S. A tuple can also be deconstructed into its first and second value by using the functions t2.fst and t2.snd respectively. For example, a tuple t1 with values (1, false) is constructed as: pvl tuple t1 = tuple { 1, false }; assert t1.fst == 1; assert t1.snd == false;  ## Examples TODO # Option The option data type is a container that either represents the presence of an element in the container or the absence of it. An option type can be constructed with the constructors Some(e) or None. The constructor Some(e) represents the presence of the value e in the option type and the constructor None represents the absence of an element. pvl option o1 = None; option o2 = Some(3);  Option types can be compared to each other where two options o3 and o4 are equivalent iff they both contain an element e3 and e4 respectively and e3 equals e4, or both are empty. pvl option o3 = Some(6); option o4 = Some(6); option o5 = Some(1); option o6 = None; assert o3 == o4; assert o4 != o5; assert o5 != o6;  ## Examples TODO # ADT Reference The tables below are a reference for all the functions/operations that are defined on the different ADTs. ## Sequence Short Description | Return type | Syntax ----------------- | ----------- | ------------- Constructor | seq | seq { e1, e2, ... }
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 | [ e1, e2, ... ]
Constructs a sequence with elements of type T initiliazed with values e1, e2, etc. This syntax requires the sequence to be initialized. Constructor | seq | [t: T ]
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 | s1 + s2 or s1.concat(s2)
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 | s1.tail
Denotes the sequence with the elements from s1 excluding the first element Prepend | seq | x::xs or xs.prepend(x)
Denotes the sequence with elements of xs prepended with the element x Slicing | seq | s1[i..j] or s1.slice(i, j)
Denotes the subsequence of sequence s1 from index i until index j (exclusive) Dropping | seq | s1[i..] or s1.drop(i)
Denotes the subsequence starting at i Taking | seq | s1[..j] or s1.take(j)
Denotes the subsequence of the first j elements Updating | seq | s1[i -> v] or s1.update(i, v)
Denotes the sequence with elements from s1 where index i has been updated to value v Removing | seq | s1.removeAt(i)
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 | set { e1, e2, ... }
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 | { e1, e2, ... }
Constructs a set with elements of type T initiliazed with values e1, e2, etc. This syntax requires the set to be initiliazed. Constructor | set | {t: T }
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 | s1 + s2 or s1.union(s2)
Denotes the set of all elements from sets s1 and s2 of the same type T Set Difference | set | s1 - s2 or s1.difference(s2)
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 | s1 * s2 or s1.intersect(s2)
Denotes the set of all elements that are both in sets s1 and s2 Set Comprehension | set | set { main \| variables; selector }
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 | bag { e1, e2, ... }
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 | b{ e1, e2, ... }
Constructs a bag with elements of type T initiliazed with values e1, e2, etc. This syntax requires the bag to be initiliazed. Constructor | bag | b{t: T }
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 | b1 + b2 or b1.sum(b2)
Denotes the bag of all elements from bags b1 and b2 of the same type T Bag Difference | bag | b1 - b2 or b1.difference(b2)
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 | b1 * b2 or b1.intersect(b2)
Denotes the bag of all elements that are both in bags b1 and b2 ## Map Short Description | Return type | Syntax ----------------- | ----------- | ------------- Constructor | map | map { k1 -> v1, k2 -> v2, ...}
Constructs a map with key-value pairs of type K and V respectively initiliazed with pairs k1,v1, k2,v2, etc. Build/Add | map | m1.add(k1, v1)
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 | m1.remove(k1)
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 | m1.keys
Returns a set of keys in map m1 Value Set | set | m1.values
Returns a set of the values in map m1 Item Set | set> | m1.items
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 | tuple {fst, snd}
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 Second Element | S | t.snd
Get the second element of the tuple t (of type tuple) ## Option Short Description | Return type | Syntax ----------------- | ----------- | ------------- Constructor | option | Some(e)
Constructs an option which contains the element e of type T Constructor | option | None
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.