Test/hofs/OneShot.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

// RUN: %dafny "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

class Ref<A> {
  var val : A;
}

method OneShot() {
  var g : () -> bool;
  var i : Ref<int>;
  i := new Ref;

  g := () -> true;

  assert g();

  i.val := i.val + 1; // heap changes

  if * {
    assert g();         // should fail
  } else {
    assert !g();        // should fail
  }
}