Mathematical types (seq, set, mset, dict)
This section gives an overview of the mathematical types supported by Gobra and their operations. Examples illustrate the syntax and the operations.
Note that mathematical types are ghost types and may only be used in ghost code.
Sequences (seq)
The type seq[T] represents finite sequences with elements of type T.
expression E | type of x | type of y | result type of E | description |
|---|---|---|---|---|
x ++ y | seq[T] | seq[T] | seq[T] | concatenation |
x[i] | seq[T] | T | lookup the element at index i 1 | |
x == y | seq[T] | seq[T] | bool | equality |
x in y | T | seq[T] | bool | true if and only if x is an element of y |
seq[T]{} | seq[T] | empty sequence | ||
seq[T]{x, y} | T | T | seq[T] | literal2 |
seq[x..y] | I | I | seq[I] 3 | integer sequence \( [x, x+1, \ldots, y-1] \) |
len(x) | seq[T] | int | length | |
x[i = y] | seq[T] | T | seq[T] | creates a sequence with element y at index i, otherwise identical to x. 1 |
x[i:j] | seq[T] | seq[T] | sub-sequence 4 | |
seq(x) | seq[T] | seq[T] | conversion from a sequence | |
seq(x) | seq[T] | [N]T | conversion from an array of length N |
1
The indices i and j are of integer type. Requires 0 <= i && i < len(x).
2
Sequence literals can be constructed with an arbitrary number of elements. The table only contains an example for two elements.
3
I is an arbitrary integer type (byte, uint8, int, ...)
4
Sub-sequence with elements between index i (inclusive) and index j (exclusive). If i < 0 or i is omitted, the lower index is treated as 0. If j > len(x) or j is omitted, the upper index is treated as len(x).
Example: seq[int]
// The empty sequence
empty := seq[int]{}
// Length of the sequence
assert len(empty) == 0
// Constructing from a literal
s := seq[int]{0, 1, 1, 2, 3}
// Membership check
assert 1 in s && !(4 in s)
// Lookup
assert s[4] == 3
// Integer sequence shorthand
s1 := seq[0..5]
// Comparison
assert seq[0..5] == seq[int]{0, 1, 2, 3, 4}
// Works also with other integer types such as byte
assert seq[0..2] == seq[byte]{byte(0), byte(1)}
assert seq[4..2] == seq[int]{}
s2 := seq[5..10]
s3 := seq[0..10]
// Concatentation of sequences with ++
assert s1 ++ s2 == s3
// Subsequences
assert s3[0:5] == s1
// Omitting the first index
assert s3[:5] == s1
// Omitting both indices
assert s3[:] == s3
// No well-defined requirements for sub-sequence indices
assert len(s3[5:1]) == 0
assert len(s3[-10:20]) == 10
// Conversion from an array
arr := [5]int{0, 1, 2, 3, 4}
s4 := seq(arr)
// Conversion from another sequence
assert s4 == seq(s4)
s5 := seq[int]{0, 0, 0}
// Create from sequence with update
s6 := s5[0 = 2]
// The original sequence is not modified (it is immutable)
assert s6[0] == 2 && s5[0] == 0
assert s5[0 = 2][1 = 4][2 = 8] == seq[int]{2, 4, 8}
Sets (set)
The type set[T] represents mathematical sets with elements of type T.
expression E | type of x | type of y | result type of E | description |
|---|---|---|---|---|
set[T]{} | set[T] | \( \varnothing \) | ||
set[T]{x, y} | T | T | set[T] | \( \{x, y \} \), in general with an arbitrary number of elements. |
x union y | set[T] | set[T] | set[T] | \( x \cup y \) |
x intersection y | set[T] | set[T] | set[T] | \( x \cap y \) |
x setminus y | set[T] | set[T] | set[T] | \( x \setminus y\) |
x subset y | set[T] | set[T] | bool | \( x \subseteq y\) |
x == y | set[T] | set[T] | bool | \( x = y\) |
x in y | T | set[T] | bool | \( x \in y\) |
len(x) | set[T] | int | \( |x| \) | |
x # y | T | set[T] | int | 1 if \(x \in y\) else 0 |
set(x) | set[T] | set[T] | conversion from a set | |
set(x) | seq[T] | set[T] | conversion from a sequence |
Example: set[int]
// The empty set
empty := seq[int]{}
s1 := set[int]{1, 2, 3}
s2 := set[int]{1, 2, 2, 3, 3, 3}
// Equality
assert s1 == s2
// Cardinality
assert len(s1) == len(s2)
// Conversion from a sequence
s3 := set(seq[int]{ 1, 2})
// Conversion from a set
s4 := set(s1)
// Membership
assert 1 in set[int]{1, 2} && !(0 in set[int]{1, 2})
// Set operations
assert set[int]{0, 2} subset set[int]{0, 1, 2}
assert set[int]{0, 2} union set[int]{1} == set[int]{0, 1, 2}
assert set[int]{0, 1} intersection set[int]{1, 2} == set[int]{1}
assert set[int]{0, 1} setminus set[int]{1, 2} == set[int]{0}
Multisets (mset)
The type mset[T] represents multisets with elements of type T.
Multisets are like sets but may contain the same element multiple times.
The multiset operations respect the multiplicities of the elements.
expression E | type of x | type of y | result type of E | description |
|---|---|---|---|---|
mset[T]{} | mset[T] | |||
mset[T]{x, x} | T | T | mset[T] | \( \{x, x \} \), in general with an arbitrary number of elements. |
x union y | mset[T] | mset[T] | mset[T] | |
x intersection y | mset[T] | mset[T] | mset[T] | |
x setminus y | mset[T] | mset[T] | mset[T] | |
x subset y | mset[T] | mset[T] | bool | |
x == y | mset[T] | mset[T] | bool | |
x in y | T | mset[T] | bool | |
len(x) | mset[T] | int | ||
x # y | T | mset[T] | int | multiplicity of the element x in y |
mset(x) | mset[T] | mset[T] | conversion from a multiset | |
mset(x) | seq[T] | mset[T] | conversion from a sequence |
Example: mset[int]
m1 := mset[int]{1, 2, 3}
m2 := mset[int]{1, 2, 2, 3, 3, 3}
assert len(m1) == 3 && len(m2) == 6
// Multiplicity
assert 3 # m1 == 1 && 3 # m2 == 3
assert 4 # m1 == 0
// multiset operations
assert mset[int]{0, 1} union mset[int]{1} == mset[int]{0, 1, 1}
assert mset[int]{1, 1, 1} intersection mset[int]{1, 1, 2} == mset[int]{1, 1}
assert mset[int]{1, 1, 2} setminus mset[int]{1, 2, 2} == mset[int]{1}
assert mset[int]{1} subset mset[int]{1, 1}
assert !(mset[int]{1, 1} subset mset[int]{1})
Dictionaries (dict)
The type dict[K]V represents dictionaries with keys of type K and values of type V.
expression E | type of x | type of y | result type of E | description |
|---|---|---|---|---|
dict[K]V{} | dict[K]V | empty dict | ||
dict[K]V{x: y} | K | V | dict[K]V | dict literal 5 |
x == y | dict[K]V | dict[K]V | bool | equality |
x[y] | dict[K]V | K | V | lookup the value associated with key y 6 |
m[x = y] | K | V | dict[K]V | dict with additional mapping (x, y), otherwise identical to the dict m |
len(x) | dict[K]V | int | number of keys | |
domain(x) | dict[K]V | set[K] | set of keys | |
range(x) | dict[K]V | set[V] | set of values |
5
In general, more items may be given. For duplicate keys, an error is reported:
m1 := dict[string]int{ "one": 1, "two": 2, "one": -1}
ERROR key appears twice in map literal
m1 := dict[string]int{ "one": 1, "two": 2, "one": -1}
^
6
Requires y in domain(x). Otherwise, an error is reported:
m1 := dict[string]int{ "one": 1, "two": 2}
assert m1["three"] == 3
ERROR Assert might fail.
Key "three" might not be contained in m1.
Example: dict[string]int
m1 := dict[string]int{ "one": 1, "two": 2}
assert m1["one"] == 1
assert len(m1) == 2
assert domain(m1) == set[string]{"one", "two"}
assert range(m1) == set[int]{1, 2}
// update dict
m2 := m1["three" = 3, "four" = 4]
// syntactic sugar for
m2 = m2["zwei" = 2]
m2["zwei"] = 2
assert m2["zwei"] == 2 && m2["three"] == 3 && m2["four"] == 4