VDM-SL cheatsheet [Types]

Comparisons

Note: the types before and after = and <> must agree.
equality = ? * ? -> bool 1 = 1
1 = 2
1 = '1'
'1' = '1'
1 = 1.0
inequality <> ? * ? -> bool 1 <> 1
1 <> 2
1 <> '1'
'1' <> '2'
1 <> 1.0
＞ > real * real -> bool 1 > 1
2 > 1
≧ >= real * real -> bool 1 >= 1
1 >= 2
＜ < real * real -> bool 1 > 1
1 > 2
≦ >= real * real -> bool 1 >= 1
2 >= 1

Numbers

Note: nat1 ⊂ nat ⊂ int ⊂ real
integer int is_int(-1)
is_int(1.0)
is_int(3.0e8)
is_int(1.01)
natural number nat is_nat(1)
is_nat(0)
is_nat(-1)
positive natural number nat1 is_nat1(1)
is_nat1(0)
real number real is_real(1)
is_real(-3.14)
integer literals 2
-1
real literals -3.14
3.0e8
1.0 = 1
addition + real * real -> real 1 + 2
subtraction - real * real -> real 1 - 2
multiplication * real * real -> real 1 * 2
division / real * real -> real 1 / 2
1 / 0
power ** real * real -> real 2 ** 3
quotient + int * int -> int 1 div 2
1 div 0
modulo mod int * int -> int 1 mod 2
-1 mod 2
1 mod -2
1 mod 0
remainder rem int * int -> int 1 rem 2
-1 rem 2
1 rem -2
1 rem 0
absolute value abs real -> real abs 2
abs -1
negation - real -> real - 3.14
-(2 + 3)
floor floor real -> int floor 3.14
floor -3.14

Booleans

boolean bool is_bool(true)
is_bool(false)
literal true
false
and, or, => are non-strict.
negation not bool -> bool not true
not false
conjunction and bool * bool -> bool true and true
true and false
true and undefined
false and undefined
undefined and false
disjunction or bool * bool -> bool false or false
true or false
true or undefined
false or undefined
undefined or true
implication => bool * bool -> bool true => true
true => false
false => false
false => undefined
undefined => true
equivalence <=> bool * bool -> bool true <=> true
false <=> false
true <=> false
inequivalence(exclusive or, xor) <> bool * bool -> bool true <> true
true <> false

Characters

character char is_char('a')
is_char('あ')
literal 'a'
'あ'
'\x41'
'\u3012'
Note: we can not order characters.
equality = char * char -> bool '1' = '1'
'1' = '2'
'A' = '\x41'
inequality <> char * char -> bool '1' <> '1'
'1' <> '2'
'A' <> '\x41'

Quote

quote <abc>, <abc_xyz> is_(<abc>, <abc>)
literal <abc>)
equality = ? * ? -> bool OK = OK
OK = ERROR
inequality <> ? * ? -> bool OK <> ERROR
OK <> OK

Tuples

product type T1 * T2 * ... * Tn is_(mk_(1,'a', 3.14), nat * char * real)
constructor mk_(1,2)
mk_(1,'a',3)
mk_(1)
element access mk_(1, 'a', 3).#1
mk_(1, 'a', 3).#2
mk_(1, 'a', 3).#3

Options / nil

types that contain nil
option type [T] is_(1, [int])
is_(nil, [int])
literal nil

Unions

union type T1 | T2 | ... | Tn is_(1, int | char)
is_('a', int | char)

Tokens

Type of uniquely mapped values from any types.
token type token is_token(mk_token(1))
is_token(mk_token('1'))
is_token(mk_token(nil))
constructor mk_token(x) mk_token(1)
mk_token("abc")
mk_token(nil)
The only available operator for token is equality and inequality. Two tokens are equal if and only if their arguments are equal.
equality = token * token -> bool mk_token(1) = mk_token(2-1)
mk_token(1) = mk_token(2)
mk_token(1) = mk_token(true)
inequality <> token * token -> bool mk_token(1) <> mk_token(2-1)
mk_token(1) <> mk_token(2)
mk_token(1) <> mk_token(true)

Records

record type T :: name1:T1 name2:T2 ... namen:Tn
T :: T1 T2 ... Tn
constructor mk_Point(1, 2.3)
field access () mk_Point(1,2).x
mk_Point(1,2).y

Sets

Finite sets
finite set type set of T is_({1,2,3}, set of nat1)
is_({}, set of nat1)
non-empty finite set type set1 of T is_({1,2,3}, set1 of nat1)
is_({}, set1 of nat1)
empty literal {}
enumeration {1,2,3}
{1,2,{'3', nil}}
section {1,...,10}
comprehension {x * 2 | x in set {1, ... ,5}}
{x * 2 | x in set {1, ... ,5} & x mod 2 = 0}
{mk_(b1, b2, b1 and b2) | b1,b2 : bool}
membership in set T * set of T -> bool 1 in set {1,2,3}
0 in set {1,2,3}
{1,2} in set {0, {1, 2}, 3}
non membership not in set T * set of T -> bool 1 not in set {1,2,3}
0 not in set {1,2,3}
{1,2} not in set {0, {1, 2}, 3}
subset subset set of T * set of T -> bool {1,2} subset {1,2,3}
{1,2,3} subset {1,2,3}
{1,2,3} subset {1,2}
proper subset psubset set of T * set of T -> bool {1,2} psubset {1,2,3}
{1,2,3} psubset {1,2,3}
{1,2,3} psubset {1,2}
union union set of T * set of T -> set of T {1,2} union {2,3}
intersection inter set of T * set of T -> set of T {1,2} inter {2,3}
difference \ set of T * set of T -> set of T {1,2} \ {2,3}
cardinality (number of elements) card set of T -> nat card {1,...,10}
card {1, 2, nil}
card {}
distributed union dunion set of set of T -> set of T dunion {{1,2}, {2,3}}
dunion {{{1},2}, {2,3}}
distributed intersection dinter set of set of T -> set of T dinter {{1,2}, {2,3}}
dinter {{1,2, {3}}, {2,3}}
power set power set of T -> set of set of T power {1,2,3}
power {}

Sequences

ordered values
sequence type seq of T is_([1,2,3], seq of nat1)
is_([], seq of nat1)
non-empty sequence type seq1 of T is_([1,2,3], seq1 of nat1)
is_([], seq1 of nat1)
empty literal []
enumeration [1,2,3]
[1,2,['3', nil]]
string literal "String"
"Str" = ['S', 't', 'r']
comprehension [x * 2 | x in set {1, ... ,5}]
[x * 2 | x in set {1, ... ,5} & x mod 2 = 0]
element access () seq of T * nat1 -> T [0,2,4](2)
[0,2,4](10)
slice ( ,..., ) seq of T * nat1 * nat1 -> T "Strings"(4,...,5)]
"Strings"(5,...,4)]
"Strings"(4,...,10)]
head element hd seq1 of T -> T hd [1,2,3]
hd "Strings"
tail elements tl seq1 of T -> seq of T tl [1,2,3]
tl "Strings"
length len seq of T -> nat len [1,2,3,4,5]
len "Strings"
elements elems seq of T -> set of T elems [1,2,3,4,5]
elems "Strings"
indices inds seq of T -> set of nat1 inds [0,2,4]
inds "Strings"
reverse reverse seq of T -> seq of T reverse [0,2,4]
reverse "Strings"
concatenation ^ seq of T * seq of T -> seq of T [0,2,4]^[1,3,5]
"Str"^"ings"
distributed concatenation conc seq of seq of T -> seq of T conc [[0,2,4],[1,3,5]]
conc ["Str","ings"]
overridng ++ seq of T * map nat1 to T -> seq of T [0,2,4]++{2|->10}
"Your"++{1|->'H'}]

map

map type map T1 to T2 is_({1|->'1', 2 |-> '2'}, map nat1 to char)
is_({1|->true, 2 |-> false, 3 |-> true, 4 |-> false}, map nat1 to bool)
injective map inmap T1 to T2 is_({1|->'1', 2 |-> '2'}, inmap nat1 to char)
is_({1|->true, 2 |-> false, 3 |-> true, 4 |-> false}, inmap nat1 to bool)
empty literal {|->}
enumeration { |-> 100, |-> 200, |-> 150}
comprehension {"0123456789"(i+1) |-> i | i in set {0,...,9}}
{"0123456789"(i+1) |-> i | i in set {0,...,9} & i mod 2 = 0}
element access () map T1 to T2 * T1 -> T2 {0 |-> false, 1 |-> true}(0)
domain dom map T1 to T2 -> set of T1 dom {0 |-> false, 1 |-> true}
range rng map T1 to T2 -> set of T2 rng {0 |-> false, 1 |-> true}
union munion map T1 to T2 * map T1 to T2 -> map T1 to T2 {0 |-> false, 1 |-> true} munion {2 |-> false, 3 |-> true}
{0 |-> false, 1 |-> true} munion {1 |-> true, 2 |-> false}
{0 |-> false, 1 |-> true} munion {1 |-> false, 2 |-> false}
overriding ++ map T1 to T2 * map T1 to T2 -> map T1 to T2 {0 |-> false, 1 |-> true} ++ {2 |-> false, 3 |-> true}
{0 |-> false, 1 |-> true} ++ {1 |-> false, 2 |-> false}
distributed union merge set of map T1 to T2 -> map T1 to T2 merge {{0 |-> false, 1 |-> true}, {2 |-> false, 3 |-> true}}
merge {{0 |-> false, 1 |-> true}, {1 |-> false, 2 |-> false}}
domain restriction <: set of T1 * map T1 to T2 -> map T1 to T2 {2,3} <: {0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true}
domain exclusion <-: set of T1 * map T1 to T2 -> map T1 to T2 {2,3} <-: {0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true}
range restriction :> map T1 to T2 * set of T2 -> map T1 to T2 {0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true} :> {true, nil}
range exclusion :-> map T1 to T2 * set of T2 -> map T1 to T2 {0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true} :-> {true, nil}
composition comp map T2 to T3 * map T1 to T2 -> map T1 to T3 {true|-><odd>, false|-><even>} comp {0 |-> false, 1 |-> true, 2 |-> false, 3 |-> true}
iteration ** map T1 to T1 * nat -> map T1 to T1 {0 |-> 1, 1 |-> 2, 2 |-> 3, 3 |-> 3} ** 1
{0 |-> 1, 1 |-> 2, 2 |-> 3, 3 |-> 3} ** 2
{0 |-> 1, 1 |-> 2, 2 |-> 3, 3 |-> 3} ** 3
inverse inverse inmap T1 to T2 -> inmap T2 to T1 inverse {0 |-> '0', 1 |-> '1', 2 |-> '2'}

Functions

Functions are values, but their equality is very tricky.
function type -> T1 * T2 * ... * Tn -> T
total function type +> T1 * T2 * ... * Tn -> T
function definition add
add(1,2)
lambda (lambda x:real, y:real & x + y)(1, 2)