diff options
Diffstat (limited to 'Test/dafny4/Primes.dfy')
| -rw-r--r-- | Test/dafny4/Primes.dfy | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Test/dafny4/Primes.dfy b/Test/dafny4/Primes.dfy index b0bb7527..fd64b45e 100644 --- a/Test/dafny4/Primes.dfy +++ b/Test/dafny4/Primes.dfy @@ -3,7 +3,7 @@ predicate IsPrime(n: int)
{
- 2 <= n && forall m :: 2 <= m < n ==> n % m != 0
+ 2 <= n && forall m {:nowarn} :: 2 <= m < n ==> n % m != 0 // WISH It would be great to think about the status of modulo as a trigger
}
// The following theorem shows that there is an infinite number of primes
@@ -167,8 +167,8 @@ lemma Composite(c: int) returns (a: int, b: int) calc {
true;
!IsPrime(c);
- !(2 <= c && forall m :: 2 <= m < c ==> c % m != 0);
- exists m :: 2 <= m < c && c % m == 0;
+ !(2 <= c && forall m {:nowarn} :: 2 <= m < c ==> c % m != 0);
+ exists m {:nowarn} :: 2 <= m < c && c % m == 0;
}
a :| 2 <= a < c && c % a == 0;
b := c / a;
@@ -194,7 +194,7 @@ lemma LargestElementExists(s: set<int>) var s' := s;
while true
invariant s' != {} && s' <= s;
- invariant forall x,y :: x in s' && y in s - s' ==> y <= x;
+ invariant forall x,y {:nowarn} :: x in s' && y in s - s' ==> y <= x;
decreases s';
{
var x :| x in s'; // pick something
|