added unit tests for exclusive refinement.

17 files changed, 435 insertions, 0 deletions

diff --git a/Test/irondafny0/FIFO.dfy b/Test/irondafny0/FIFO.dfy
new file mode 100644
index 00000000..1256b55d
--- /dev/null
+++ b/Test/irondafny0/FIFO.dfy
@@ -0,0 +1,43 @@
+// RUN: %dafny /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..bac08fba
--- /dev/null
+++ b/Test/irondafny0/LIFO.dfy
@@ -0,0 +1,43 @@
+// RUN: %dafny /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..9f7eb534
--- /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 as 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..eaadc85a
--- /dev/null
+++ b/Test/irondafny0/inheritreqs0.dfy.expect
@@ -0,0 +1,6 @@
+inheritreqs0.dfy(19,14): Error BP5002: A precondition for this call might not hold.

+inheritreqs0.dfy[Impl](6,18): 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..27c76fee
--- /dev/null
+++ b/Test/irondafny0/inheritreqs1.dfy.expect
@@ -0,0 +1,6 @@
+inheritreqs1.dfy(20,14): Error BP5002: A precondition for this call might not hold.

+inheritreqs1.dfy(15,18): 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/xrefine0.dfy b/Test/irondafny0/xrefine0.dfy
new file mode 100644
index 00000000..35993ce8
--- /dev/null
+++ b/Test/irondafny0/xrefine0.dfy
@@ -0,0 +1,6 @@
+// RUN: %dafny /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..10d25f53
--- /dev/null
+++ b/Test/irondafny0/xrefine1.dfy
@@ -0,0 +1,77 @@
+// RUN: %dafny /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 as 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 as HostSpec

+    import PI as 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..ae844fc8
--- /dev/null
+++ b/Test/irondafny0/xrefine1.dfy.expect
@@ -0,0 +1,6 @@
+xrefine1.dfy(71,13): Error BP5002: A precondition for this call might not hold.

+xrefine1.dfy[MainImpl](49,29): 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..7578b424
--- /dev/null
+++ b/Test/irondafny0/xrefine2.dfy
@@ -0,0 +1,77 @@
+// RUN: %dafny /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 as 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 as HostSpec

+    import PI as 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..69c5bc27
--- /dev/null
+++ b/Test/irondafny0/xrefine3.dfy
@@ -0,0 +1,72 @@
+// RUN: %dafny /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 as 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 as AlphaSpec

+    import B as 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!