audit format

dafny-lang · Feb 29, 2024 · 16b5021 · 16b5021
1 parent e1f5f34
commit 16b5021
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/src/Util/FisherYates/Correctness.dfy b/src/Util/FisherYates/Correctness.dfy
@@ -24,7 +24,7 @@ module FisherYates.Correctness {
     iset s | Model.Shuffle(xs, i)(s).Result? && Model.Shuffle(xs, i)(s).value[i..] == p[i..]
   }
 
-  ghost predicate CorrectnessPredicate<T(!new)>(xs: seq<T>, p: seq<T>, i: nat) 
+  ghost predicate CorrectnessPredicate<T(!new)>(xs: seq<T>, p: seq<T>, i: nat)
     requires i <= |xs|
     requires i <= |p|
   {
@@ -244,7 +244,7 @@ module FisherYates.Correctness {
       reveal BitStreamsInA;
       assert e' in Rand.eventSpace && Rand.prob(e') == 1.0 / (NatArith.FactorialTraditional(|xs|-(i+1)) as real) by {
         assert e' in Rand.eventSpace by {
-          assert CorrectnessPredicate(ys, p, i+1) by { reveal InductionHypothesis; } 
+          assert CorrectnessPredicate(ys, p, i+1) by { reveal InductionHypothesis; }
           assert e' == CorrectnessConstructEvent(ys, p, i+1);
         }
         calc {

diff --git a/src/Util/FisherYates/Model.dfy b/src/Util/FisherYates/Model.dfy
@@ -38,8 +38,8 @@ module FisherYates.Model {
       var ys := Swap(xs, i, j);
       var r := ShuffleCurried(ys, s', i + 1);
       assert forall j | 0 <= j < i :: ShuffleInvariancePredicatePointwise(xs, r, j) by {
-        forall j | 0 <= j < i 
-          ensures ShuffleInvariancePredicatePointwise(xs, r, j) 
+        forall j | 0 <= j < i
+          ensures ShuffleInvariancePredicatePointwise(xs, r, j)
         {
           assert ShuffleInvariancePredicatePointwise(ys, r, j);
         }