Axiomatic Data Types

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 (for sequences sets and bags) and here (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.

seq<int> s1 = seq<int> { 1, 2, 3 };
seq<int> s2 = seq<int> { };

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.

seq<int> s3 = [ 1, 2, 3 ];
seq<int> 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.

seq<int> s5 = [ 1, 2, 4, 8, 16 ];
assert s5[3] == 8;
assert |s5| == 5;
assert s5 == seq<int> { 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.

seq<int> s6 = [ 1, 2, 4, 8, 16 ];
assert 0::s6 == [ 0, 1, 2, 4, 8, 16 ];

seq<int> 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..].

seq<int> 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:

pure boolean sorted(seq<int> 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:

pure boolean distinct(seq<int> 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:

requires |xs| > 0;
ensures (\forall int i; 0 <= i && i < |xs|; xs[i] <= \result);
pure static int max(seq<int> 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.

set<int> s1 = set<int> { 1, 2, 3, 2 };
set<int> s2 = set<int> { };

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.

set<int> s3 = { 1, 2, 2, 3 };
set<int> 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.

set<int> s5 = { 1, 2, 2, 3 };
set<int> s6 = { 3, 4, 5, 6 };
set<int> s7 = { 1, 2 };
set<int> 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.

set<int> s5 = { 1, 2, 2, 3 };
set<int> 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<T> { 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<int> {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:

class SetComp {
    requires 0 <= j && j < 5;
    void myMethod(int j) {
       set<int> a = set<int> {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.

bag<int> b1 = bag<int> { 1, 2, 3, 2 };
bag<int> b2 = bag<int> { };

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.

bag<int> b3 = b{ 1, 2, 2, 3 };
bag<int> 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.

bag<int> b5 = b{ 1, 2, 2, 3 };
bag<int> b6 = b{ 3, 4, 5, 6, 5 };
bag<int> b7 = b{ 1, 2, 3, 2, 2, 6 };
bag<int> 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.

bag<int> b9 = bag<int> { 3 };
bag<int> b10 = bag<int> { 3, 4 };
bag<int> b11 = bag<int> { 1, 2, 2, 3 };
bag<int> b12 = bag<int> { 2, 3, 3, 4 };
bag<int> b13 = bag<int> { 1, 1, 2, 3 };
bag<int> b14 = bag<int> { 2, 3, 3, 4 };

assert b9 + b10 == bag<int> { 3, 3, 4 };
assert b12 - b11 == bag<int> { 3, 4 };
assert b11 - b12 == bag<int> { 1, 2 };
assert b13 * b14 == bag<int> { 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<K,V> { 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.

map<int, boolean> m1 = map<int,boolean>{1 -> true, 2 -> true, 0 -> false};
map<int, boolean> m2 = map<int,boolean>{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.

map<int, boolean> m1 = map<int,boolean>{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<int, boolean> { 0, false } \in m1.items;
assert tuple<int, boolean> { 1, true } \in m1.items;
assert tuple<int, boolean> { 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).

map<int, int> m1 = map<int,int>{};
map<int, int> m2 = m1.add(1, 1).add(2, 4).add(3, 9);
map<int, int> m3 = m2.remove(2);
map<int, int> 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<F,S> { 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:

tuple<int, boolean> t1 = tuple<int, boolean> { 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.

option<int> o1 = None;
option<int> 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.

option<int> o3 = Some(6);
option<int> o4 = Some(6);
option<int> o5 = Some(1);
option<int> 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<T>	seq<T> { 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<T>	[ 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: 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 `
Comparison	boolean	s1 == s2 Returns true if s1 and s2 are equivalent
Concatenation	seq<T>	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<T>	s1.tail Denotes the sequence with the elements from s1 excluding the first element
Prepend	seq<T>	x::xs or xs.prepend(x) Denotes the sequence with elements of xs prepended with the element x
Slicing	seq<T>	s1[i..j] or s1.slice(i, j) Denotes the subsequence of sequence s1 from index i until index j (exclusive)
Dropping	seq<T>	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<T>	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<T>	set<T> { 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<T>	{ 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: 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 `
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<T>	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<T>	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<T>	s1 * s2 or s1.intersect(s2) Denotes the set of all elements that are both in sets s1 and s2
Set Comprehension	set<T>	set<T> { 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<T>	bag<T> { 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<T>	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<T>	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 `
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<T>	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<T>	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<T>	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<K,V>	map<K,V> { 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<K,V>	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<K,V>	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 `
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<K>	m1.keys Returns a set of keys in map m1
Value Set	set<V>	m1.values Returns a set of the values in map m1
Item Set	set<tuple<K,V>>	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<F,S>	tuple<F,S> {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<F,S>)
Get Second Element	S	t.snd Get the second element of the tuple t (of type tuple<F,S>)

Option

Short Description	Return type	Syntax
Constructor	option<T>	Some(e) Constructs an option which contains the element e of type T
Constructor	option<T>	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:

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.