From 014fc54f9dd27d458b656b7aedf402dbb4f9c16a Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 15 Apr 2014 16:55:47 -0700
Subject: Cleaned up some no longer needed parentheses in test file

---
 Test/VSComp2010/Problem2-Invert.dfy | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'Test/VSComp2010')

diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy
index 0f7c50c1..327703e7 100644
--- a/Test/VSComp2010/Problem2-Invert.dfy
+++ b/Test/VSComp2010/Problem2-Invert.dfy
@@ -24,26 +24,26 @@
 
 method M(N: int, A: array<int>, B: array<int>)
   requires 0 <= N && A != null && B != null && N == A.Length && N == B.Length && A != B;
-  requires (forall k :: 0 <= k && k < N ==> 0 <= A[k] && A[k] < N);
-  requires (forall j,k :: 0 <= j && j < k && k < N ==> A[j] != A[k]);  // A is injective
-  requires (forall m :: 0 <= m && m < N && inImage(m) ==> (exists k :: 0 <= k && k < N && A[k] == m));  // A is surjective
+  requires forall k :: 0 <= k < N ==> 0 <= A[k] < N;
+  requires forall j,k :: 0 <= j < k < N ==> A[j] != A[k];  // A is injective
+  requires forall m :: 0 <= m < N && inImage(m) ==> exists k :: 0 <= k && k < N && A[k] == m;  // A is surjective
   modifies B;
-  ensures (forall k :: 0 <= k && k < N ==> 0 <= B[k] && B[k] < N);
-  ensures (forall k :: 0 <= k && k < N ==> B[A[k]] == k && A[B[k]] == k);  // A and B are each other's inverses
-  ensures (forall j,k :: 0 <= j && j < k && k < N ==> B[j] != B[k]);  // (which means that) B is injective
+  ensures forall k :: 0 <= k < N ==> 0 <= B[k] < N;
+  ensures forall k :: 0 <= k < N ==> B[A[k]] == k == A[B[k]];  // A and B are each other's inverses
+  ensures forall j,k :: 0 <= j < k < N ==> B[j] != B[k];  // (which means that) B is injective
 {
   var n := 0;
-  while (n < N)
+  while n < N
     invariant n <= N;
-    invariant (forall k :: 0 <= k && k < n ==> B[A[k]] == k);
+    invariant forall k :: 0 <= k < n ==> B[A[k]] == k;
   {
     B[A[n]] := n;
     n := n + 1;
   }
-  assert (forall i :: 0 <= i && i < N ==> A[i] == old(A[i]));  // the elements of A were not changed by the loop
+  assert forall i :: 0 <= i < N ==> A[i] == old(A[i]);  // the elements of A were not changed by the loop
   // it now follows from the surjectivity of A that A is the inverse of B:
-  assert (forall j :: 0 <= j && j < N && inImage(j) ==> 0 <= B[j] && B[j] < N && A[B[j]] == j);
-  assert (forall j,k :: 0 <= j && j < k && k < N ==> B[j] != B[k]);
+  assert forall j :: 0 <= j < N && inImage(j) ==> 0 <= B[j] < N && A[B[j]] == j;
+  assert forall j,k :: 0 <= j < k < N ==> B[j] != B[k];
 }
 
 static function inImage(i: int): bool { true }  // this function is used to trigger the surjective quantification
@@ -73,7 +73,7 @@ method PrintArray(a: array<int>)
   requires a != null;
 {
   var i := 0;
-  while (i < a.Length) {
+  while i < a.Length {
     print a[i], "\n";
     i := i + 1;
   }
-- 
cgit v1.2.3