Суть этого доказательства должна показать, что процедура «слияния» вставляет каждый элемент один и только один раз в результат. Поскольку процедура слияния работает с использованием цикла, вам нужно использовать инвариант цикла , чтобы показать это.
Инварианты цикла обычно можно обнаружить, спросив: «Что я знаю на полпути? через цикл? "
to merge arrays A and B:
let n = length of A, m = length of B
let R = new array of length (n + m)
let i = 0, j = 0
while i < n or j < m:
if i < n and (j == m or A[i] <= B[j]):
R[i+j] = A[i]
i = i + 1
else:
R[i+j] = B[j]
j = j + 1
return R
В этом цикле мы всегда знаем, что первые i + j элементы R являются некоторой перестановкой первых i элементов A и первых j элементов BЭто инвариант цикла, поэтому вам нужно показать, что:
- Это верно до начала цикла (когда i = j = 0).
- Если это верно доитерации цикла, то после этой итерации она остается истинной, то есть инвариант сохраняется.
- Если это так, когда цикл завершается (когда i = m, j = n), то массив R имеетобязательное свойство.
В общем, сложные части доказательства, подобные этому, обнаруживают инвариант цикла и показывают, что инвариант сохраняется при каждой итерации цикла.