summaryrefslogtreecommitdiff
path: root/Test/test21/InterestingExamples4.bpl
blob: 67636af1d40426c4816fa119d47e112495cb6659 (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
36
37
38
39
40
41
42
// a property that should hold according to the Boogie semantics
// (but no automatic theorem prover will be able to prove it)


type C a;

function sameType<a,b>(x:a, y:b) returns (bool);

axiom (forall<a,b> x:a, y:b :: sameType(x,y) == (exists z:a :: y==z));

// Will be defined to hold whenever the type of y (i.e., b)
// can be reached from the type of x (a) by applying the type
// constructor C a finite number of times. In order words,
// b = C^n(a)
function rel<a,b>(x:a, y:b) returns (bool);

function relHelp<a,b>(x:a, y:b, z:int) returns (bool);

axiom (forall<a, b> x:a, y:b :: relHelp(x, y, 0) == sameType(x, y));
axiom (forall<a, b> n:int, x:a, y:b ::
 (n >= 0 ==>
   relHelp(x, y, n+1) ==
   (exists<c> z:c, y' : C c :: relHelp(x, z, n) && y==y')));

axiom (forall<a, b> x:a, y:b ::
 rel(x, y) == (exists n:int :: n >= 0 && relHelp(x, y, n)));

// Assert that from every type we can reach a type that is
// minimal, i.e., that cannot be reached by applying C to some
// other type. This will only hold in well-founded type
// hierarchies

procedure P() returns () {
  var v : C int;

  assert relHelp(7, 13, 0);
  assert rel(7, 13);

  assert (forall<b> y:b :: (exists<a> x:a ::               // too hard for a theorem prover
   rel(x, y) &&
   (forall<c> z:c :: (rel(z, x) ==> sameType(z, x)))));
}