From fad74b96e5d9367960358b1c4cc9c2cce79e961a Mon Sep 17 00:00:00 2001 From: Michael Lowell Roberts Date: Wed, 8 Jul 2015 11:01:11 -0700 Subject: added unit tests for exclusive refinement. --- Test/irondafny0/FIFO.dfy | 43 ++++++++++++++++++ Test/irondafny0/FIFO.dfy.expect | 8 ++++ Test/irondafny0/LIFO.dfy | 43 ++++++++++++++++++ Test/irondafny0/LIFO.dfy.expect | 8 ++++ Test/irondafny0/Queue.dfyi | 22 ++++++++++ Test/irondafny0/inheritreqs0.dfy | 22 ++++++++++ Test/irondafny0/inheritreqs0.dfy.expect | 6 +++ Test/irondafny0/inheritreqs1.dfy | 22 ++++++++++ Test/irondafny0/inheritreqs1.dfy.expect | 6 +++ Test/irondafny0/xrefine0.dfy | 6 +++ Test/irondafny0/xrefine0.dfy.expect | 2 + Test/irondafny0/xrefine1.dfy | 77 +++++++++++++++++++++++++++++++++ Test/irondafny0/xrefine1.dfy.expect | 6 +++ Test/irondafny0/xrefine2.dfy | 77 +++++++++++++++++++++++++++++++++ Test/irondafny0/xrefine2.dfy.expect | 9 ++++ Test/irondafny0/xrefine3.dfy | 72 ++++++++++++++++++++++++++++++ Test/irondafny0/xrefine3.dfy.expect | 6 +++ 17 files changed, 435 insertions(+) create mode 100644 Test/irondafny0/FIFO.dfy create mode 100644 Test/irondafny0/FIFO.dfy.expect create mode 100644 Test/irondafny0/LIFO.dfy create mode 100644 Test/irondafny0/LIFO.dfy.expect create mode 100644 Test/irondafny0/Queue.dfyi create mode 100644 Test/irondafny0/inheritreqs0.dfy create mode 100644 Test/irondafny0/inheritreqs0.dfy.expect create mode 100644 Test/irondafny0/inheritreqs1.dfy create mode 100644 Test/irondafny0/inheritreqs1.dfy.expect create mode 100644 Test/irondafny0/xrefine0.dfy create mode 100644 Test/irondafny0/xrefine0.dfy.expect create mode 100644 Test/irondafny0/xrefine1.dfy create mode 100644 Test/irondafny0/xrefine1.dfy.expect create mode 100644 Test/irondafny0/xrefine2.dfy create mode 100644 Test/irondafny0/xrefine2.dfy.expect create mode 100644 Test/irondafny0/xrefine3.dfy create mode 100644 Test/irondafny0/xrefine3.dfy.expect (limited to 'Test/irondafny0') 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 + + 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) 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 + + predicate IsValid(b:Beta) { + forall i :: 0 <= i < |b| ==> A.IsValid(b[i]) + } + + method Init(ays:seq) 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! -- cgit v1.2.3