sorting_tutorial_2: THEORY BEGIN %%% %%% This is a tutorial example for modeling a sequential program on %%% arrays. We'll use "bubble sort" for our example, and let our %%% array be indexed by natural numbers. Also fix some program %%% variables to range over array indices. %%% a, b: VAR ARRAY [nat -> int] %%% %%% Define predicates specifying correctness for a sorting %%% algorithm on arrays. The elements should be in non-decreasing %%% order; and the content should be unchanged. To support %%% partial computation of inner loops, these predicates must %%% be parameterized by an index range (bounds l and u). %%% l,u: VAR nat % These are always used for upper and lower array bounds z: VAR int % Always used for some item in an array sorted?(a, l, u):bool = forall( j:{i:nat | l <= i AND i < u}): a(j) <= a(j+1) occurrences(z, a, l, u): RECURSIVE nat = IF l > u THEN 0 ELSE (IF (a(l) = z) THEN 1 ELSE 0 ENDIF) + occurrences(z, a, l+1, u) ENDIF MEASURE u-l % This isn't going to work! sorted_lemma_1: LEMMA FORALL (a:[nat -> int], l:nat, u:{i:nat | l <= i}): sorted?(a, l, u) IFF FORALL (j:{i:nat | l <= i AND i <= u}, k:{i:nat | j <= i AND i <=u}): sorted?(a, j, k) permutation?(a, b, l, u):bool = forall z: occurrences(z, a, l, u) = occurrences(z, b, l, u) permutation_lemma_1: LEMMA permutation?(a, b, l, u) IMPLIES FORALL (k:{i:nat | l <= i AND i <= u}): EXISTS (j:{i:nat | l <= i AND i <= u}): a(k) = b(j) permutation_lemma_2: LEMMA FORALL (a:[nat -> int], l:nat, u:{i:nat | l <= i}, j,k:{i:nat | l <= i AND i <= u}): permutation?(a, a WITH [(j):= a(k), (k):= a(j)], l, u) %%% %%% Probably useful facts about sorted arrays and permutations. %%% generalized_sorted?: LEMMA sorted?(a, l, u) IFF forall (j, k:{i:nat | l <= i AND i <= u}): j <= k IMPLIES a(j) <= a(k) %%% %%% Fix an initial array and range over which sorting is to %%% to be done. For simplicity, we'll set the lower bound to %%% be 0. (The bounds would better be fixed as theory parameters) %%% A_0: ARRAY [nat -> int] N: nat %%% %%% Here is a sequential program claimed to perform a Bubble Sort. %%% Note that it is not the same computation as Bsort, in the first tutorial. %%% %%% { a[0..N] A A_0[0..N] } %%% %%% k := N; %%% while (L < k) {INV1 ?} %%% begin %%% j := 0; %%% while (j < k) {INV2 ?} %%% begin %%% if a[J] > a[J+1] %%% then a[J], a[J+1] := a[J+1], a[J] %%% else skip; %%% j:= j+1 %%% end; %%% k := k-1 %%% end %%% end %%% %%% { permutation?(a[0..N], A_0[0..N]) } %%% { sorted?(a[0..N] } %%% %%% The correctness assertion says that when the program terminates %%% the final content of A is the same as its initial content, and %%% has been sorted. %%% %%% We need to devise loop invariants to support the desired %%% post conditions: %%% %%% Outer loop: The outer loop should not change the content of %%% if the array and is intended to get the largest elements %%% to the high end of the list. So, %%% %%% INV1 == permutation?(a[0..N], A_0[0..N]) & sorted?(a[K..N]) %%% %%% INV1 is true initially, and when the loop test fails, it implies %%% that sorted?(a[0..N]). %%% %%% Inner loop: The inner loop is supposed to make INV1 true once %%% k has been decremented. Assuming INV1 is true, once its %%% test fails the largest element in a[0..K] will be in the %%% in the highest position, so a[0..(k-1)] is sorted. %%% %%% INV2 == j <= k & (forall 0 <= i < j : a[i] <= a[j]) %%% %%% Translation to PVS: %%% j,k: VAR nat BS_inner_loop(l:nat, u:{i:nat | l <= i}, a): RECURSIVE ARRAY [nat -> int] = IF l = u THEN a ELSE IF a(l) > a(l+1) THEN BS_inner_loop(l+1, u, a WITH [(l) := a(l+1), (l+1) := a(l)]) ELSE BS_inner_loop(l+1, u, a) ENDIF ENDIF MEASURE u-l by < BS_outer_loop(l:nat, u:{i:nat | l <= i}, a): RECURSIVE ARRAY [nat -> int] = IF l = u THEN a ELSE BS_outer_loop(l, u-1, BS_inner_loop(l, u, a)) ENDIF MEASURE u-l by < BSort(a): ARRAY [nat -> int] = BS_outer_loop(0, N, a) BS_inner_loop_correct_x: LEMMA FORALL (l:nat, u:{i:nat | l <= i}): LET b = BS_inner_loop(l, u, a) IN FORALL (i:nat): l <= i AND i <= u IMPLIES b(i) <= b(u) BS_inner_loop_correct_z: LEMMA FORALL (l:nat, u:{i:nat | l <= i}, a): LET b = BS_inner_loop(l, u, a) IN (FORALL (i:nat): (l <= i AND i <= u IMPLIES b(i) <= b(u)) AND (i < l OR u < i IMPLIES b(i) = a(i))) BS_inner_loop_no_side_effects: LEMMA FORALL (l:nat, u:{i:nat | l <= i}, a): FORALL (k:{i:nat | i