Test/dafny0/ComputationsNeg.dfy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

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);
}