summaryrefslogtreecommitdiff
path: root/Test/test20/Prog0.bpl
blob: ea71b8a8223235ddd9d050228b97115632316f46 (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
26
27
28
29
30
31
32
33
34
35
// Let's test some Boogie 2 features ...
type real;
type elements;

type Field a;
var heap : <a> [ref, Field a] a;

const emptyset : <a> [a] bool;

function union(<a> [a] bool, <a> [a] bool) returns (<a> [a] bool);

axiom (forall x : <a> [a] bool, y : <a> [a] bool,
              z : int ::         
              { union(x, y)[z] } 
              union(x, y)[z] == (x[z] || y[z]));

var tau : <a> [ref] int;             // error: type variable has to occur in arguments

axiom (forall x : int :: !emptyset[x]);

// the more general version of the axiom that also uses type quantifiers

axiom (forall<alpha>
              x : <a> [a] bool, y : <a> [a] bool,
              z : alpha ::         
              { union(x, y)[z] } 
              union(x, y)[z] == (x[z] || y[z]));

axiom (forall<beta, alpha, beta> a:alpha, b:beta ::        // error: variable bound twice
              a == b ==> (exists c:alpha :: c == b));

axiom (forall<beta> a:alpha, b:beta ::                     // error: alpha is not declared
              a == b ==> (exists c:alpha :: c == b));

type ref;