Test/dafny0/Include.dfy


1
2
3
4
5
6
7
8
9
10
11
12


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