Test/dafny0/Include.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

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

include "Includee.dfy"

method test_include(z:int)
{
  // Make sure we can still see function bodies
  assert forall y :: f(y) == 2*y;

  // Use an unverified method
  var w := m_unproven(z);
  assert w == 2*z;
}

// and some refinement stuff, to make sure it works with includes
module Concrete refines Abstract
{
  function method inc...  // error: postcondition violation
  {
    x - 1
  }
  method M...
  {
    var y := G(x);  // error: it is not know whether or not G(x) is non-negative, as required
    if x < 68 {
      return 70;  // error
    } else if 30 <= x {  // this will always be true here
      return x;  // fine
    }
    ...;
  }
}