Test/dafny4/Bug110.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

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

module Io {
  predicate AdvanceTime(oldTime:int) { oldTime > 2 }
  class Time
  {
    static method GetTime()
        ensures AdvanceTime(1);        
  }

  function MaxPacketSize() : int { 65507 }

  class UdpClient
  {
    method Receive()        
        ensures AdvanceTime(3);       

    method Send() returns(ok:bool)
        requires 0 <= MaxPacketSize();       
  }
}

abstract module Host {
    import opened Io // Doesn't work.   
    //import Io          // Works
}

abstract module Main {
    import H : Host
}