Test/dafny0/AssumptionVariables1.dfy


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

// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

method test0(x: int)
{
  ghost var {:assumption} a0: bool;
  ghost var {:assumption} a1: bool, a2: bool, {:assumption} a3: bool;

  assert a0 && a1 && a3;

  a0 := a0 && (0 < x);

  a1 := a1 && true;
}


method test1(x: int)
{
  ghost var {:assumption} a0: bool;

  assert a0;

  a0 := a0 && (0 < x);

  var y := x;

  while (y < 0)
  {
    ghost var {:assumption} a0: bool;

    assert a0;

    a0 := a0 && (0 < y);

    y := y + 1;
  }
}