blob: a4fa7de6fc8888b8daf6599e7bd1e0c0206d5e41 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
// RUN: %boogie -noVerify "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// set of maps from anything to a specific type a
const mapSet : <a>[<b>[b]a]bool;
const emptySet : <a>[a]bool;
axiom mapSet[5]; // type error
axiom mapSet[emptySet] == true;
axiom mapSet[emptySet := false] != mapSet;
axiom mapSet[emptySet := 5] == mapSet; // type error
axiom emptySet[13 := true][13] == true;
axiom (forall f : <c>[c]int, x : ref :: mapSet[f] ==> f[x] >= 0);
axiom (forall f : <c>[c]c :: mapSet[f]); // type error
axiom mapSet[mapSet] == true; // type error
type ref;
|
