Fix 2020 permutations insertion.pvl

utwente-fmt · Jun 29, 2023 · c34bc0d · c34bc0d
1 parent 7e21aac
commit c34bc0d
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/examples/publications/2020/permutations/insertion.pvl b/examples/publications/2020/permutations/insertion.pvl
@@ -81,7 +81,7 @@ class BubbleSort {
 		int k = 0;
 
 		loop_invariant 0 <= k && k <= |xs|;
-		loop_invariant (\forall int l; l>=0 && l<k; counter(xs + ys, xs[l]) == counter(xs, xs[l]) + counter(ys, xs[l]));
+		loop_invariant (\forall int l; l>=0 && l<k; {: counter(xs + ys, xs[l]) :} == counter(xs, xs[l]) + counter(ys, xs[l]));
 		while(k < |xs|)
 		{
 			lemma_count_app(xs, ys, xs[k]);
@@ -157,7 +157,7 @@ class BubbleSort {
 		int k = 0;
 
 		loop_invariant 0 <= k && k <= |xs|;
-		loop_invariant (\forall int l; l>=0 && l<k; counter(xs, xs[l]) == counter(ys, xs[l]));
+		loop_invariant (\forall int l; l>=0 && l<k; {: counter(xs, xs[l]) :} == counter(ys, xs[l]));
 		while(k < |xs|)
 		{
 			lemma_swap_permutation(xs, ys, i, j, xs[k]);