diff options
| author |  leino <unknown> | 2014-08-28 11:59:20 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-08-28 11:59:20 -0700 |
| commit | db4d9e34aa774f3167a4842aaf75221bc24d50bc (patch) | |
| tree | bf5a5a8727d245e0171f8095204eff9aad927e93 /Test | |
| parent | 565b411b3dafa597232f99c018a11163dcda5175 (diff) | |
Bounds discovery now takes newtype constraints into consideration.
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/DiscoverBounds.dfy | 51 | ||||
| -rw-r--r-- | Test/dafny0/DiscoverBounds.dfy.expect | 4 |
2 files changed, 55 insertions, 0 deletions
diff --git a/Test/dafny0/DiscoverBounds.dfy b/Test/dafny0/DiscoverBounds.dfy new file mode 100644 index 00000000..ea3f8cff --- /dev/null +++ b/Test/dafny0/DiscoverBounds.dfy @@ -0,0 +1,51 @@ +// RUN: %dafny /print:"%t.print" /compile:3 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+newtype NT = x | 0 <= x < 100
+newtype UT = NT
+
+newtype Lower = x | 10 <= x
+newtype Upper = x: Lower | x < 100
+
+newtype Int = int
+
+newtype NR = r | -2.0 <= r <= 5.4
+
+method Main()
+{
+ var n: NT :| true;
+ var t: UT :| true;
+
+ var u: Upper :| true;
+ var l: Lower :| l < 20;
+ var o: Lower :| true;
+
+ var j: Int :| true;
+
+ print n, "\n";
+ print t, "\n";
+ print u, "\n";
+ print l, "\n";
+ print o, "\n";
+
+ var b: bool;
+ b := forall n': NT :: true ==> P(int(n'));
+ b := forall t': UT :: true ==> P(int(t'));
+ b := forall u': Upper :: true ==> P(int(u'));
+ b := forall l': Lower :: l' < 20 ==> P(int(l'));
+ b := forall o': Lower :: true ==> P(int(o')); // error: cannot find finite range
+ b := forall j': Int :: -3 <= j' < 7 ==> P(int(j'));
+
+ b := forall r: real :: 0.0 <= r <= 100.0 ==> Q(r); // error: cannot find finite range
+ b := forall r': NR :: true ==> Q(real(r')); // error: cannot find finite range
+}
+
+predicate method P(x: int)
+{
+ x == 157
+}
+
+predicate method Q(r: real)
+{
+ r / 2.0 <= r
+}
diff --git a/Test/dafny0/DiscoverBounds.dfy.expect b/Test/dafny0/DiscoverBounds.dfy.expect new file mode 100644 index 00000000..ee816683 --- /dev/null +++ b/Test/dafny0/DiscoverBounds.dfy.expect @@ -0,0 +1,4 @@ +DiscoverBounds.dfy(36,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o''
+DiscoverBounds.dfy(39,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'r'
+DiscoverBounds.dfy(40,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'r''
+3 resolution/type errors detected in DiscoverBounds.dfy
|