blob: 0c5391176609492a063e910354653f46f8b660a3 (
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
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
function bad(n: nat): nat
decreases n;
{
bad(n+1)
}
ghost method go_bad()
ensures bad(0)==0;
{
}
datatype Nat = Zero | Succ(tail: Nat)
predicate ThProperty(step: nat, t: Nat, r: nat)
{
match t
case Zero => true
case Succ(o) => step>0 && exists ro:nat :: ThProperty(step-1, o, ro)
}
ghost method test_ThProperty()
ensures ThProperty(10, Succ(Zero), 0);
{
// assert ThProperty(9, Zero, 0);
}
// The following is a test that well-typedness antecednets are included in the literal axioms
function StaticFact(n: nat): nat
ensures 0 < StaticFact(n);
{
if n == 0 then 1 else n * StaticFact(n - 1)
}
method test_StaticFact()
{
assert StaticFact(0) == 1;
assert 42 != 42; // error: this should fail
}
function fact(n: nat): nat
{
if (n==0) then 1 else n*fact(n-1)
}
method test_fact()
{
assert fact(0) == 1;
assert 42 != 42; // error: this should fail
}
|
