Test/irondafny0/inheritreqs1.dfy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

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

abstract module Spec {
    method Greet(b: bool)
        requires b;
}

module Impl refines Spec {
    method Greet(b: bool) {
        print "o hai!\n";
    }

    method Xyzzy(b: bool)
        requires b;
    {}

    method Main() {
        Greet(true);
        Xyzzy(false);
    }
}