Test/dafny4/Bug125.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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58

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

abstract module AbstractModuleA 
{
  type T
} 

abstract module AbstractModuleB 
{
  import opened AMA : AbstractModuleA

  method Foo(t:T)
} 

abstract module AbstractModuleC refines AbstractModuleB 
{
  import opened AMA2 : AbstractModuleA
}

module LibA {
  class G { 
    static function f(x:int) : bool {
      x >= 10
    }
  }

  function g() : bool {
     true
  }
}

module LibB {
  class G { 
    static function f(x:int) : bool {
      x < 10
    }
  }

  function g() : bool {
     false
  }
}

module R {
  import opened LibA
}

module S refines R {
  import opened LibB
  method m() {
    assert g();  // should be LibA.g
  }

  method m1() {
   assert G.f(20); // should be LibA.G.f
  }
}