blob: c27fa82c4f5ca3b39569bdbbbf77bc103a8295e3 (
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
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
|
// RUN: %dafny "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
function method MkId<A>() : A -> A {
x => x
}
function method IntId() : int -> int {
y => y
}
function method DivZero() : int -> int
{
z => 5 / z // div by zero
}
function method DivZeroWithReq() : int -> int
{
(z) requires z != 0 => 5 / z
}
function method DivZero2() : (int, int) -> int {
(x, y) requires y != 0 => x / y
}
function method DivZero3() : int -> int {
z => z / 0 // div by zero
}
function method Shadow() : int -> real -> real {
x => x => x
}
method Reqs() {
var fn := (u) requires u => u;
print fn(true);
print fn(false); // precond violation
}
method Main() {
var id := IntId();
print id(5);
var polyid : int -> int := MkId();
print polyid(5);
assert id(2) == polyid(2);
assert id(3) != 4 && 5 != polyid(6);
var divvy := DivZero2();
print divvy(2,5);
print divvy(2,0); // precond violation
}
function method succ(x : int) : int
requires x > 0;
{
x + 1
}
method Main2() {
var suc := succ;
assert suc(3) == succ(3);
assert suc(-1) == 0; // precond violation
}
function method Id<A>(x : A) : A {
x
}
method Main3() {
var id := Id;
assert id(3) == 3;
assert forall x :: (Id(id))(x) == (y => y)(x);
assert forall x :: (Id(id))(x) == (y => y)(2); // should fail
}
function P(f: A -> B, x : A): B
reads (f.reads)(x);
requires (f.requires)(x);
{
f(x)
}
function Q(f: U -> V, x : U): V
reads P.reads(f,x);
requires f.requires(x); // would be nice to be able to write P.requires(f,x)
{
P(f,x)
}
function QQ(f: U -> V, x : U): V
reads ((() => ((()=>f)()).reads)())((()=>x)());
requires ((() => ((()=>f)()).requires)())((()=>x)());
{
((() => P)())((()=>f)(),(()=>x)())
}
|
