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

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

newtype Byte = x | 0 <= x < 256
predicate method GoodByte(b: Byte) {
  b % 3 == 2
}
predicate method GoodInteger(i: int) {
  i % 5 == 4
}

method Main() {
  assert GoodByte(11) && GoodInteger(24);
  var b: Byte :| GoodByte(b);
  var i: int :| 0 <= i < 256 && GoodInteger(i);
  print "b=", b, "  i=", i, "\n";
  var m0 := new MyClass;
  var m17 := new M17.AnotherClass;
}

class MyClass { }

module M17 {
  class AnotherClass { }
}