diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-15 22:02:08 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-15 22:02:08 -0700 |
| commit | 650ad1ee685b599b08717a3d83a31c0689b006e9 (patch) | |
| tree | d549727eaca8de47028f53cb648d6a95e6e3a0c4 /Test/dafny0/NonGhostQuantifiers.dfy | |
| parent | f2153b5cfdeaf57fac07583b0cc82a9ea283e34a (diff) | |
Dafny: added optional range expressions to logical quantifiers, preparing for addition other other comprehensions (like set comprehension)
Diffstat (limited to 'Test/dafny0/NonGhostQuantifiers.dfy')
| -rw-r--r-- | Test/dafny0/NonGhostQuantifiers.dfy | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/Test/dafny0/NonGhostQuantifiers.dfy b/Test/dafny0/NonGhostQuantifiers.dfy index ea256a58..58e64827 100644 --- a/Test/dafny0/NonGhostQuantifiers.dfy +++ b/Test/dafny0/NonGhostQuantifiers.dfy @@ -33,6 +33,23 @@ class MyClass<T> { (forall n :: 2 <= n ==> 1000 <= n || (exists d :: n < d && d < 2*n))
}
+ function method GoodRange(): bool
+ {
+ (forall n | 2 <= n :: 1000 <= n || (exists d | n < d :: d < 2*n)) && (exists K: nat | K < 100 :: true)
+ }
+ function method BadRangeForall(): bool
+ {
+ forall n | n <= 2 :: 1000 <= n || n % 2 == 0 // error: cannot bound range for n
+ }
+ function method BadRangeExists(): bool
+ {
+ exists d | d < 1000 :: d < 2000 // error: cannot bound range for d
+ }
+ function method WhatAboutThis(): bool
+ {
+ forall n :: 2 <= n && (forall M | M == 1000 :: n < M) ==> n % 2 == 0 // error: heuristics don't get this one for n
+ }
+
// Here are more tests
function method F(a: array<T>): bool
|