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

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

method m_unproven(x:int) returns (y:int)
  ensures y == 2*x;
{  // error: postcondition violation
}

function f(x:int) : int
{
  2*x
}

abstract module Abstract
{
  function method inc(x:int) :int
    ensures inc(x) > x;

  method M(x: int) returns (r: int)
    ensures r == x;
  {  // error: postcondition violation
    var y :| 0 <= y;
    r := x + 3;
    assert r % 3 == 0;  // error
  }

  function method G(x: int): int
}