скачать doc
.
4. КОРРЕКТНОСТЬ ПРОГРАММ ПРИ РАБОТЕ С МАССИВАМИ
На основе сформулированных ранее правил вывода операторов языка Паскаль и правил верификации программ далее рассматриваются вопросы верификации и проектирования программ, работающих с массивами. Вводятся новые способы записи утверждений (предикатов), расширяющие возможности верификации программ при работе с массивами. Использование кванторов позволяет формулировать утверждения о массивах или об их частях.
4.1. Кванторы и запись утверждений о массивах
Квантор существования. Пусть m и n – выражения с целочисленными значениями (m n). Рассмотрим предикат
Pm or P m + 1 or ... or Pn 1, (4.1)
где каждое Pi – предикат. Предикат (4.1) истинен, если истинно хотя бы одно из Pi. Недостатком такой формы записи является то, что здесь используется знак «...», апеллирующий к интуиции читателя. Предикат (4.1) можно записать в другой форме, использующей квантор существования :
( i: m i < n: Pi). (4.2)
Здесь i называется квантифицированной переменной, а неравенство m i < n задает область её значений. На естественном языке (4.2) читается следующим образом: существует по крайней мере одно (целое) значение i, лежащее между m и n 1 (включительно), для которого выполнено утверждение Pi.
Используемые в математике способы записи сумм и произведений тоже могут рассматриваться как кванторы:
Их иногда записывают в форме
что совсем близко к виду (4.2). Далее там, где удобно, будем записывать их в виде
( i: m i < n: ai), ( i: m i < n: ai).
Формально квантор существования можно определить рекурсивно (так же как и кванторы и ср. с определением индуктивных функций в разд. 3) следующим образом.
Определение :
1) для n = m : ( i: m i < m: Pi) = false,
2) для n = k + 1 > m: ( i: m i < k + 1: Pi) = ( i: m i < k: Pi) or Pk.
Следует обратить внимание на базис этого рекурсивного (индуктивного) определения. При пустой области значений квантифицированной переменной дизъюнкция нуля предикатов есть false. Например, ( i: 0 i < 0: 22=4) = false. Это аналогично определениям ( i: m i < m: ai) = 0, ( i: m i < m: ai) = 1, а также определениям f(), используемым в разд. 3.
Квантор всеобщности. Содержательно определим квантор всеобщности (читается: «для всех») как
( i: m i < n: Pi) = Pm & P m + 1 & ... & Pn 1.
Формально можно либо дать рекурсивное определение, аналогичное определению квантора , либо определить квантор всеобщности через квантор , подчеркивая тот факт, что с формальной точки зрения лишь один из этих кванторов является новым понятием. Действительно, используя законы отрицания и де Моргана, получаем
Pm & P m + 1 & ... & Pn 1 = not not (Pm & P m + 1 & ... & Pn 1 ) =
= not (not Pm or not P m + 1 or ... or not Pn 1) = not ( i: m i < n: not Pi),
что дает возможность определить квантор через квантор .
Определение : ( i: m i < n: Pi) = not ( i: m i < n: not Pi).
Из этого определения следует, что
( i: m i < m: Pi) = not ( i: m i < m: not Pi) = not false = true.
В качестве упражнения определите квантор всеобщности рекурсивно (подобно данному ранее определению квантора существования).
Квантор количества (счёта). Для количества различных значений i из области m i < n, при которых истинно Pi, удобно иметь специальное обозначение ( i: m i < n: Pi) .
Дадим формальное определение (по существу, это определение некоторой индуктивной функции).
Определение :
1) для n = m : ( i: m i < m: Pi) = 0,
2) для n = k +1 > m: (i: m i < k + 1: Pi)=
= ( i: m i < k: Pi)+(if Pk then 1 else 0).
Заметим, что кванторы существования и всеобщности можно выразить через квантор количества:
( i: m i < n: Pi) = ( ( i: m i < n : Pi) 1),
( i: m i < n: Pi) = ( ( i: m i < n : Pi) = n m).
В качестве примера использования квантора количества приведем ситуацию, когда нужно записать утверждение о том, что k второе по величине из чисел, для которых выполняется Pk (из ряда возможных P0, P1, ...). Если бы требовалось найти наименьшее k, при котором истинно Pk, то это можно было бы выразить таким образом: (k 0) & ( i: 0 i < k: not Pi) & Pk.
Утверждение о втором по величине k выглядит уже более громоздко:
(k 0) & (0 j < k) & ( i: 0 i < j: not Pi) & Pj & ( i: j + 1 i < k: not Pi) & Pk,
не говоря уже об утверждениях относительно третьего и следующих по величине k. С помощью квантора счёта все эти утверждения можно записать лаконичнее и яснее:
для первого k: ( ( i: 0 i < k : Pi) = 0 ) & Pk,
для второго k: ( ( i: 0 i < k : Pi) = 1 ) & Pk, ...
для -го по величине k: ( ( i: 0 i < k : Pi) = 1 ) & Pk.
Замечание 1. Можно доопредилить введенные кванторы на тот случай, когда область значений квантифицированной переменной включает правую границу n, например:
( i: m i n: Pi) = ( i: m i < n + 1: Pi).
Замечание 2. Кванторы с прилегающими друг к другу областями можно соединять следующим образом:
( i: m i < n: Pi) or ( i: n i < q: Pi) = ( i: m i < q: Pi) ,
( i: m i < n: Pi) & ( i: n i < q: Pi) = ( i: m i < q: Pi) ,
( i: m i < n: Pi) + ( i: n i < q: Pi) = ( i: m i < q: Pi) .
Рассмотрим примеры записи утверждений о массивах с помощью кванторов. Пусть имеется массив a[1..n] и целые переменные j и k, такие, что 1 j k + 1 n + 1. Запись a[j..k] обозначает отрезок (или сегмент) массива. Первый элемент этого сегмента есть a[j], а последний a[k]. При j = k + 1 сегмент пуст. В каждом приведенном ниже примере даны содержательная и формальная формулировки утверждения:
1) все элементы a[j..k] нулевые: ( i: j i < k + 1: a[i] = 0);
2) все элементы a[j..k] ненулевые: ( i: j i < k + 1: a[i] 0), или not ( i: j i < k + 1: a[i] = 0);
3) значения элементов a[j..k] расположены в возрастающем порядке: ( i: j i < k: a[i] < a[i + 1]);
4) любой элемент a[1..j] меньше y, а любой элемент a[j+1..n] больше y: (0 j n) & ( i: 1 i < j + 1: a[i] < y) & ( i: j + 1 i < n + 1: a[i] > y);
5) значение y встречается в массивах b[1..n] и c[1..m] одинаковое число раз: ( i: 1 i n: b[i] = y) = ( i: 1 i m: c[i] = y).
Сокращения. В некоторых случаях удобно использовать сокращенную запись утверждений о массивах, например:
Предикат Сокращение
( i: 1 i < j + 1: a[i] < y) a[1..j] < y
( i: j i < k + 1: a[i] = 0) a[j..k] = 0
( i: j i < k + 1: a[i] = y) y a[j..k]
Картинки массивов. Многие часто встречающиеся утверждения о массивах легче понять, если представить их в форме так называемых картинок. При этом важно, что каждую картинку можно при необходимости заменить на эквивалентный ей предикат. Например, картинка
| | 1 | j k | n | |
| a: | ? | = 0 | ? | & (1 j k + 1 n + 1) |
эквивалентна предикату (1 j k + 1 n + 1) & ( i: j i < k + 1: a[i] = 0), а картинка
-
1 j
n
a:
< y
> y
& (0 j n )
эквивалентна предикату
(0 j n ) & ( i: 1 i < j + 1: a[i] < y) & ( i: j + 1 i < n + 1: a[i] > y).
В дальнейшем картинки будут регулярно использоваться для записи утверждений о массивах.
4.2. Правила вывода для цикла с параметром
Для определения правила вывода цикла for необходимо сделать следующее ограничение: тело цикла не может изменить значения параметра цикла и границ цикла. Именно таким свойством обладает цикл for в Паскале. Введем обозначения для открытых и замкнутых интервалов: [a..b] { ia i b}, [a..b) { ia i < b},
(a..b] { ia < i b}, (a..b) { ia < i < b}.
Заметим, что [a..a) (b..b] [ ], где [ ] обозначает пустой интервал. Введем также обозначения для утверждения P(w) относительно интервала w:
P([a..b]) ( ia i b: Pi), P([a..b)) ( ia i < b: Pi),
P((a..b]) ( ia < i b: Pi), P((a..b)) ( ia < i < b: Pi).
Рассмотрим оператор цикла for i := a to b do S. В соответствии с семантикой этого оператора параметр цикла при выполнении пробегает последовательность значений
a, succ(a), succ(succ(a)), ..., pred(b), b. (4.3)
Предположим, что тело цикла S обладает свойством
{P([a..i))} S {P([a..i])}. (4.4)
При этом говорят, что тело цикла S действует на утверждение P индуктивно. Тогда, согласно (4.3) и (4.4), после первой итерации будет выполняться P([a..a]), после второй P([a..succ(a)]) и т. д. Наконец, при завершении последней итерации получим P([a..b]). Если дополнительно предположить, что P([a..a)), т. е. P([ ]) истинно, то из приведенных рассуждений следует правило вывода
{ (a i b) & P([a..i))} S {P([a..i])}
. (4.5)
{P([ ])} for i := a to b do S {P([a..b])}
Утверждение P([a..i)) является инвариантом точки входа в тело цикла, а утверждение P([a..i]) инвариантом точки выхода из него. Далее будем называть P([a..i]) и P([a..i)) индуктивными утверждениями цикла с параметром for i := a to b do S.
Заметим, что в случае цикла for (в отличие от циклов while-do и repeat-until) проблема завершимости цикла не возникает. В силу семантики цикла for для его завершения достаточно, чтобы завершилось выполнение S(i) при всех i из интервала a i b.
Аналогичным образом можно получить правило вывода для цикла for i := b downto a do S:
{(a i b) & P((i..b])} S {P([i..b])}
. (4.6)
{P([ ])} for i := b downto a do S {P([a..b])}
4.3. Примеры программ работы с массивами
Пример 1. Рассмотрим применение правила вывода для цикла с параметром в задаче нахождения максимального элемента заданного массива a[1..n]. Пусть требуется найти номер m максимального элемента, т. е. такое m, что (1 m n) & ( j: 1 j n: a[m] a[j]).
Очевидное решение состоит в просмотре всех элементов массива, реализуемом с помощью цикла for-to-do. Тогда постусловие этого цикла есть
P([1..n]) (1 m n) & ( j: 1 j n: a[m] a[j]),
а индуктивные утверждения P([1..i]) и P([1..i)) имеют вид:
P([1..i]) (1 m i) & ( j: 1 j i: a[m] a[j]),
P([1..i)) (1 m < i) & ( j: 1 j < i: a[m] a[j]),
При этом P([1..1)) true. По смыслу на i-м шаге значение m номер максимального элемента в просмотренной части a[1..i]. Решением задачи будет цикл {n>0} m := 1; for i := 1 to n do ТЕЛО ЦИКЛА. В соответствии с правилом вывода (4.5) тело цикла должно действовать индуктивно на P([1..i]), т. е. {P([1..i))} ТЕЛО ЦИКЛА {P([1..i])}.
Содержательно понятно, что расширить область истинности утверждения P(*) от [1..i) до [1..i] можно сравнением текущего максимума a[m] с добавляемым элементом a[i]:
m := 1; for i := 1 to n do if a[i] > a[m] then m := i .
В качестве упражнения, используя правила вывода условного оператора и оператора присваивания, докажите, что
{ P([1..i)) } if a[i] > a[m] then m := i { P([1..i]) }.
Замечание 1. Ясно, что при n >1 цикл можно начать с i = 2, т. е.
m := 1; for i := 2 to n do if a[i] > a[m] then m := i .
Замечание 2. Полезно сравнить решение этой задачи с решением задачи для последовательности, читаемой из файла (см. 3.2).
Пример 2. Вычисление суммы элементов массива a[1..n]
Естественным в этой задаче выглядит применение цикла с параметром for i := 1 to n do. Постусловие этого цикла запишем в виде
P([1..n]) (s = ( j: 1 j n: a[j])).
Тело цикла должно индуктивно действовать на утверждение
P([1..i]) (s = ( j: 1 j i: a[j])).
Преобразовать утверждение
P([1..i)) (s = ( j: 1 j < i: a[j]))
в утверждение P([1..i]) можно оператором s := s + a[i].
Для цикла for i := n downto 1 do по правилу(4.6) аналогично имеем:
P([i..n]) (s = ( j: i j n: a[j]),
P((i..n]) (s = ( j: i < j n: a[j]),
что приводит к такому же телу цикла. Таким образом, имеем два симметричных решения:
1) s := 0; for i := 1 to n do s := s + a[i];
2) s := 0; for i := n downto 1 do s := s + a[i].
Следующий пример демонстрирует тот факт, что подобная симметрия имеется не всегда и использование цикла for-downto-do может оказаться предпочтительным.
Пример 3. Вычисление значения полинома
pn(x) = a1 + a2 x1 + a3 x2 +...+ an xn 1
где n порядок (количество коэффициентов) полинома.
Введем более детальные обозначения:
указав в качестве дополнительных аргументов (или параметров) функции p() порядок полинома n и набор коэффициентов a[1..n], где a[i] соответствует ai.
Рассмотрим также полином, определяемый отрезком массива a[k..m] при 1 k m n:
Как и в предыдущем примере, рассмотрим постусловие
P([1..n]) ( p = p(n, a[1..n]; x))
и две его модификации, соответствующие двум видам цикла с параметром:
P([1..j]) ( p = p(j, a[1..j]; x)), (4.7)
P([j..n]) ( p = p(n j + 1, a[j..n]; x)). (4.8)
Первый вариант (4.7), как легко видеть, приводит к программе
p := 0; z := 1;