diff options
| author |  Michael Lowell Roberts <mirobert@microsoft.com> | 2015-07-08 11:01:11 -0700 |
|---|---|---|
| committer | Michael Lowell Roberts <mirobert@microsoft.com> | 2015-07-08 11:01:11 -0700 |
| commit | fad74b96e5d9367960358b1c4cc9c2cce79e961a (patch) | |
| tree | 805771f13c38cc2206ee9f6d6226651db5b61573 /Test/irondafny0/xrefine3.dfy | |
| parent | 85d4456ccf1e1d8c456dffa012d3f3d724f50a4a (diff) | |
added unit tests for exclusive refinement.
Diffstat (limited to 'Test/irondafny0/xrefine3.dfy')
| -rw-r--r-- | Test/irondafny0/xrefine3.dfy | 72 |
1 files changed, 72 insertions, 0 deletions
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
+}
+
+
+
+
|