21 files changed, 471 insertions, 0 deletions
diff --git a/Test/irondafny0/FIFO.dfy b/Test/irondafny0/FIFO.dfy
new file mode 100644
index 00000000..ded8f567
--- /dev/null
+++ b/Test/irondafny0/FIFO.dfy
@@ -0,0 +1,43 @@
+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+include "Queue.dfyi"
+
+module FIFO exclusively refines Queue {
+    type Item = int
+
+    method Init() returns (q: Queue) {
+        q := [];
+    }
+
+    method Push(item: Item, q: Queue) returns (q': Queue) {
+        return q + [item];
+    }
+
+    method Pop(q: Queue) returns (item: Item, q': Queue)
+        ensures item == q[0]
+    {
+        item := q[0];
+        q' := q[1..];
+    }
+}
+
+module MainImpl refines MainSpec {
+    import Q = FIFO
+
+    method Main()
+    {
+        var q := Q.Init();
+        q := Q.Push(0, q);
+        q := Q.Push(1, q);
+        q := Q.Push(2, q);
+
+        var n: int;
+        n, q := Q.Pop(q);
+        print n, "\n";
+        n, q := Q.Pop(q);
+        print n, "\n";
+        n, q := Q.Pop(q);
+        print n, "\n";
+    }
+}
diff --git a/Test/irondafny0/FIFO.dfy.expect b/Test/irondafny0/FIFO.dfy.expect
new file mode 100644
index 00000000..25021947
--- /dev/null
+++ b/Test/irondafny0/FIFO.dfy.expect
@@ -0,0 +1,8 @@
+
+Dafny program verifier finished with 8 verified, 0 errors
+Program compiled successfully
+Running...
+
+0
+1
+2
diff --git a/Test/irondafny0/LIFO.dfy b/Test/irondafny0/LIFO.dfy
new file mode 100644
index 00000000..8c0a08e8
--- /dev/null
+++ b/Test/irondafny0/LIFO.dfy
@@ -0,0 +1,43 @@
+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+include "Queue.dfyi"
+
+module LIFO exclusively refines Queue {
+    type Item = int
+
+    method Init() returns (q: Queue) {
+        q := [];
+    }
+
+    method Push(item: Item, q: Queue) returns (q': Queue) {
+        return [item] + q;
+    }
+
+    method Pop(q: Queue) returns (item: Item, q': Queue)
+        ensures item == q[0]
+    {
+        item := q[0];
+        q' := q[1..];
+    }
+}
+
+module MainImpl refines MainSpec {
+    import Q = LIFO
+
+    method Main()
+    {
+        var q := Q.Init();
+        q := Q.Push(0, q);
+        q := Q.Push(1, q);
+        q := Q.Push(2, q);
+
+        var n: int;
+        n, q := Q.Pop(q);
+        print n, "\n";
+        n, q := Q.Pop(q);
+        print n, "\n";
+        n, q := Q.Pop(q);
+        print n, "\n";
+    }
+}
diff --git a/Test/irondafny0/LIFO.dfy.expect b/Test/irondafny0/LIFO.dfy.expect
new file mode 100644
index 00000000..83f90a5b
--- /dev/null
+++ b/Test/irondafny0/LIFO.dfy.expect
@@ -0,0 +1,8 @@
+
+Dafny program verifier finished with 8 verified, 0 errors
+Program compiled successfully
+Running...
+
+2
+1
+0
diff --git a/Test/irondafny0/Queue.dfyi b/Test/irondafny0/Queue.dfyi
new file mode 100644
index 00000000..06f4b29e
--- /dev/null
+++ b/Test/irondafny0/Queue.dfyi
@@ -0,0 +1,22 @@
+// Queue.dfyi
+
+abstract module Queue {
+    type Item
+    type Queue = seq<Item>
+
+    method Init() returns (q: Queue)
+        ensures |q| == 0;
+
+    method Push(item: Item, q: Queue) returns (q': Queue)
+        ensures |q'| == |q| + 1;
+
+    method Pop(q: Queue) returns (item: Item, q': Queue)
+        requires |q| > 0;
+        ensures item in q;
+        ensures |q'| == |q| - 1;
+}
+
+abstract module MainSpec {
+    import Q : Queue
+}
+
diff --git a/Test/irondafny0/inheritreqs0.dfy b/Test/irondafny0/inheritreqs0.dfy
new file mode 100644
index 00000000..a0117da0
--- /dev/null
+++ b/Test/irondafny0/inheritreqs0.dfy
@@ -0,0 +1,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(false);
+        Xyzzy(false);
+    }
+}
diff --git a/Test/irondafny0/inheritreqs0.dfy.expect b/Test/irondafny0/inheritreqs0.dfy.expect
new file mode 100644
index 00000000..44e33bc0
--- /dev/null
+++ b/Test/irondafny0/inheritreqs0.dfy.expect
@@ -0,0 +1,6 @@
+inheritreqs0.dfy(19,13): Error BP5002: A precondition for this call might not hold.
+inheritreqs0.dfy[Impl](6,17): Related location: This is the precondition that might not hold.
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 6 verified, 1 error
diff --git a/Test/irondafny0/inheritreqs1.dfy b/Test/irondafny0/inheritreqs1.dfy
new file mode 100644
index 00000000..c83d04ac
--- /dev/null
+++ b/Test/irondafny0/inheritreqs1.dfy
@@ -0,0 +1,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);
+    }
+}
diff --git a/Test/irondafny0/inheritreqs1.dfy.expect b/Test/irondafny0/inheritreqs1.dfy.expect
new file mode 100644
index 00000000..a07d179d
--- /dev/null
+++ b/Test/irondafny0/inheritreqs1.dfy.expect
@@ -0,0 +1,6 @@
+inheritreqs1.dfy(20,13): Error BP5002: A precondition for this call might not hold.
+inheritreqs1.dfy(15,17): Related location: This is the precondition that might not hold.
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 6 verified, 1 error
diff --git a/Test/irondafny0/opened_workaround.dfy b/Test/irondafny0/opened_workaround.dfy
new file mode 100644
index 00000000..6d44ccfd
--- /dev/null
+++ b/Test/irondafny0/opened_workaround.dfy
@@ -0,0 +1,21 @@
+// RUN: %dafny /ironDafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module A {
+
+    predicate P() 
+
+    class C
+    {
+        static method{:axiom} M()
+            ensures P();
+    } 
+}
+
+abstract module B {
+    import opened A
+}
+
+abstract module C {
+    import Bee : B       // Works
+}
diff --git a/Test/irondafny0/opened_workaround.dfy.expect b/Test/irondafny0/opened_workaround.dfy.expect
new file mode 100644
index 00000000..0be94b4c
--- /dev/null
+++ b/Test/irondafny0/opened_workaround.dfy.expect
@@ -0,0 +1,3 @@
+
+Dafny program verifier finished with 3 verified, 0 errors
+Compilation error: Function _0_A_Compile._default.P has no body
diff --git a/Test/irondafny0/optimize0.dfy b/Test/irondafny0/optimize0.dfy
new file mode 100644
index 00000000..865d8707
--- /dev/null
+++ b/Test/irondafny0/optimize0.dfy
@@ -0,0 +1,6 @@
+// RUN: %dafny /compile:3 /optimize /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main() {
+    print "o hai!";
+}
diff --git a/Test/irondafny0/optimize0.dfy.expect b/Test/irondafny0/optimize0.dfy.expect
new file mode 100644
index 00000000..6b3e13c5
--- /dev/null
+++ b/Test/irondafny0/optimize0.dfy.expect
@@ -0,0 +1,6 @@
+
+Dafny program verifier finished with 2 verified, 0 errors
+Program compiled successfully
+Running...
+
+o hai!
+\ No newline at end of file
diff --git a/Test/irondafny0/xrefine0.dfy b/Test/irondafny0/xrefine0.dfy
new file mode 100644
index 00000000..b849111c
--- /dev/null
+++ b/Test/irondafny0/xrefine0.dfy
@@ -0,0 +1,6 @@
+// RUN: %dafny /ironDafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+abstract module Delicious {}
+module Chocolate exclusively refines Delicious {}
+module Strawberry exclusively refines Delicious {}
diff --git a/Test/irondafny0/xrefine0.dfy.expect b/Test/irondafny0/xrefine0.dfy.expect
new file mode 100644
index 00000000..136e06db
--- /dev/null
+++ b/Test/irondafny0/xrefine0.dfy.expect
@@ -0,0 +1,2 @@
+xrefine0.dfy(6,7): Error: no more than one exclusive refinement may exist for a given module.
+1 resolution/type errors detected in xrefine0.dfy
diff --git a/Test/irondafny0/xrefine1.dfy b/Test/irondafny0/xrefine1.dfy
new file mode 100644
index 00000000..1b835649
--- /dev/null
+++ b/Test/irondafny0/xrefine1.dfy
@@ -0,0 +1,77 @@
+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+abstract module ProtocolSpec {
+    type ProtoT
+
+    predicate Init(p:ProtoT)
+}
+
+abstract module HostSpec {
+    type HostT
+    import P : ProtocolSpec
+
+    function method foo(h:HostT) : P.ProtoT
+}
+
+module ProtocolImpl exclusively refines ProtocolSpec {
+    type ProtoT = bool    
+
+    predicate Init(p:ProtoT) { !p }
+
+    method orange(i:nat) returns (j:nat)
+    {
+        j := i + 1;
+    }
+}
+
+module HostImpl exclusively refines HostSpec {
+    import P = ProtocolImpl
+
+    type HostT = int
+
+    function method foo(h:HostT) : P.ProtoT
+    {
+        h > 0
+    }
+
+    method apple(i:nat) returns (j:nat)
+    {
+        j := i + 1;
+    }
+}
+
+abstract module MainSpec {
+    import HI : HostSpec
+    import PI : ProtocolSpec
+
+    method Test(h1:HI.HostT, h2:HI.HostT) 
+        requires HI.foo(h1) == HI.foo(h2);
+        requires PI.Init(HI.foo(h1))
+}
+
+module MainImpl exclusively refines MainSpec {
+    import HI = HostImpl
+    import PI = ProtocolImpl
+    
+    method Test(h1:HI.HostT, h2:HI.HostT) 
+    {
+        var a := HI.foo(h1);
+        print "HI.foo(h1) => ", a, "\n";
+        var b := HI.foo(h2);
+        print "HI.foo(h2) => ", b, "\n";
+        var i := PI.orange(1);
+        print "PI.orange(1) => ", i, "\n";
+        var j := HI.apple(2);
+        print "PI.apple(2) => ", j, "\n";
+    }
+
+    method Main()
+    {
+        Test(-1, 1);
+    }
+}
+
+
+
+
diff --git a/Test/irondafny0/xrefine1.dfy.expect b/Test/irondafny0/xrefine1.dfy.expect
new file mode 100644
index 00000000..ec946cda
--- /dev/null
+++ b/Test/irondafny0/xrefine1.dfy.expect
@@ -0,0 +1,6 @@
+xrefine1.dfy(71,12): Error BP5002: A precondition for this call might not hold.
+xrefine1.dfy[MainImpl](49,28): Related location: This is the precondition that might not hold.
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 12 verified, 1 error
diff --git a/Test/irondafny0/xrefine2.dfy b/Test/irondafny0/xrefine2.dfy
new file mode 100644
index 00000000..9c33391b
--- /dev/null
+++ b/Test/irondafny0/xrefine2.dfy
@@ -0,0 +1,77 @@
+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+abstract module ProtocolSpec {
+    type ProtoT
+
+    predicate Init(p:ProtoT)
+}
+
+abstract module HostSpec {
+    type HostT
+    import P : ProtocolSpec
+
+    function method foo(h:HostT) : P.ProtoT
+}
+
+module ProtocolImpl exclusively refines ProtocolSpec {
+    type ProtoT = bool    
+
+    predicate Init(p:ProtoT) { p }
+
+    method orange(i:nat) returns (j:nat)
+    {
+        j := i + 1;
+    }
+}
+
+module HostImpl exclusively refines HostSpec {
+    import P = ProtocolImpl
+
+    type HostT = int
+
+    function method foo(h:HostT) : P.ProtoT
+    {
+        h != 0
+    }
+
+    method apple(i:nat) returns (j:nat)
+    {
+        j := i + 1;
+    }
+}
+
+abstract module MainSpec {
+    import HI : HostSpec
+    import PI : ProtocolSpec
+
+    method Test(h1:HI.HostT, h2:HI.HostT) 
+        requires HI.foo(h1) == HI.foo(h2);
+        requires PI.Init(HI.foo(h1))
+}
+
+module MainImpl exclusively refines MainSpec {
+    import HI = HostImpl
+    import PI = ProtocolImpl
+    
+    method Test(h1:HI.HostT, h2:HI.HostT) 
+    {
+        var a := HI.foo(h1);
+        print "HI.foo(h1) => ", a, "\n";
+        var b := HI.foo(h2);
+        print "HI.foo(h2) => ", b, "\n";
+        var i := PI.orange(1);
+        print "PI.orange(1) => ", i, "\n";
+        var j := HI.apple(2);
+        print "PI.apple(2) => ", j, "\n";
+    }
+
+    method Main()
+    {
+        Test(-1, 1);
+    }
+}
+
+
+
+
diff --git a/Test/irondafny0/xrefine2.dfy.expect b/Test/irondafny0/xrefine2.dfy.expect
new file mode 100644
index 00000000..6d3fecd4
--- /dev/null
+++ b/Test/irondafny0/xrefine2.dfy.expect
@@ -0,0 +1,9 @@
+
+Dafny program verifier finished with 13 verified, 0 errors
+Program compiled successfully
+Running...
+
+HI.foo(h1) => True
+HI.foo(h2) => True
+PI.orange(1) => 2
+PI.apple(2) => 3
diff --git a/Test/irondafny0/xrefine3.dfy b/Test/irondafny0/xrefine3.dfy
new file mode 100644
index 00000000..86dbd957
--- /dev/null
+++ b/Test/irondafny0/xrefine3.dfy
@@ -0,0 +1,72 @@
+// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+abstract module AlphaSpec {
+    type Alpha
+
+    predicate IsValid(a:Alpha)
+
+    method Init() returns (a:Alpha)
+        ensures IsValid(a);
+}
+
+abstract module BetaSpec {
+    type Beta
+    import A : AlphaSpec
+
+    predicate IsValid(b:Beta)
+
+    method Init(ays:seq<A.Alpha>) returns (b:Beta)
+        requires forall i :: 0 <= i < |ays| ==> A.IsValid(ays[i]);
+        ensures IsValid(b);
+}
+
+module AlphaImpl exclusively refines AlphaSpec {
+    type Alpha = bool    
+
+    predicate IsValid(a:Alpha) { 
+        a 
+    }
+
+    method Init() returns (a:Alpha)
+        ensures IsValid(a);
+    {
+        a := true;
+    }
+}
+
+module BetaImpl exclusively refines BetaSpec {
+    import A = AlphaImpl
+    type Beta = seq<A.Alpha>
+
+    predicate IsValid(b:Beta) {
+        forall i :: 0 <= i < |b| ==> A.IsValid(b[i])
+    }
+
+    method Init(ays:seq<A.Alpha>) returns (b:Beta) {
+        b := ays;
+    }
+}
+
+abstract module MainSpec {
+    import A : AlphaSpec
+    import B : BetaSpec
+
+    method Main()
+    {
+        var a := A.Init();
+        var ays := [a, a];
+        assert forall i :: 0 <= i < |ays| ==> A.IsValid(ays[i]);
+        var b := B.Init(ays);
+        print "o hai!\n";
+    }
+}
+
+module MainImpl exclusively refines MainSpec {
+    import B = BetaImpl
+    import A = AlphaImpl
+}
+
+
+
+
diff --git a/Test/irondafny0/xrefine3.dfy.expect b/Test/irondafny0/xrefine3.dfy.expect
new file mode 100644
index 00000000..1e5a5b4e
--- /dev/null
+++ b/Test/irondafny0/xrefine3.dfy.expect
@@ -0,0 +1,6 @@
+
+Dafny program verifier finished with 14 verified, 0 errors
+Program compiled successfully
+Running...
+
+o hai!