Сборник задач по курсу «Теория вычислительных процессов» (стр. 7 )

14. На одном из языков программирования напишите программу вычисления наибольшего произведения элементов строк матрицы AM×N, но вычисление произведения элементов каждой строки матрицы оформите в виде подпрограммы. Докажите правильность написанной программы.

Задания повышенной сложности

15. Предположим, что два массива целых чисел упорядочены в возрастающем порядке X (1: M), Y (1: N) (т. е. нет одинаковых элементов и X(1) < X(2) < ... < X(M), Y(1) < Y(2) < ... < Y(N)). На одном из языков программирования напишите программу создающую и печатающую два массива:
UNION(1: L1), INTERSECTION (1: L2). Массивы построены следующим образом: UNION(1: L1) содержит в возрастающем (без повторений) порядке все элементы, имеющиеся либо в X (1: M), либо в Y (1: N), либо в X (1: M) и Y (1: N); INTERSECTION (1: L2) содержит в возрастающем порядке (без повторений) все элементы, которые есть и в X (1: M), и в Y (1: N). Докажите правильность написанной программы.

16. На одном из языков программирования напишите программу, которая читает на входе любое положительное число и проверяет, совершенно ли оно. Число N называется совершенным, если и только если оно есть сумма всех целых I, удовлетворяющих условию 1 ≤ I < N и делящих N без остатка. Например, 6 – совершенное число, ибо 6 = 1 + 2 + 3. Докажите правильность программы.

17. Предположим, что имеется массив целых чисел X (1: N), содержащий только значения 1 и 2. . На одном из языков программирования напишите программу упорядочения на основе принципа «смены мест» (т. е. в программе значения X(I) изменяются только путем «обмена» значением с некоторым X(J), причем считать число элементов каждого типа запрещено). Время работы такой программы пропорционально N и программа заканчивается за один проход по массиву. Докажите правильность написанной программы.

18. Докажите правильность программы, если условия задачи аналогичны задаче 17, но в массив встречаются лишь значения 1, 2 и 3.

19. На одном из языков программирования напишите программу для формирования и печати в возрастающем порядке N наименьших элементов из последовательности  1, 2, 3, 4, 6, 8, 9, 12, 16, 18, ... . Последовательность образована по следующим правилам:

а) 1 – первый элемент последовательности;

б) если s принадлежит последовательности, то 2⋅s и 3⋅s также принадлежат последовательности;

в) в последовательности нет других элементов, кроме тех, которые удовлетворяют первым двум правилам.

Тема 5. ФОРМАЛИЗАЦИЯ ДОКАЗАТЕЛЬСТВА правильности
С ПОМОЩЬЮ ИДУКТИВНЫХ УТВЕРЖДЕНИЙ

Используя какую-либо формальную нотацию для записи индуктивных утверждений и соответствующую дедуктивную систему для проведения доказательств, то можно формализовать весь процесс доказательства правильности методом индуктивных утверждений. Обсудим некоторые аспекты такой формализации. Наиболее изученной формальной нотацией для формулирования и проведения математического доказательства является исчисление предикатов.

Напомним, что метод индуктивных утверждений состоит в следующем [1]. Для доказательства частичной правильности некоторой блок-схемы относительно утверждений А и С мы связываем утверждение А с начальной точкой блок-схемы, а утверждение С – с конечной. Кроме этого, необходимо выделить и связать с блок-схемой некоторые другие утверждения (описывающие отношения между значениями переменных, справедливые в момент попадания в соответствующую точку программы). Нужно, в частности, связать по крайней мере с одной из точек в замкнутом пути (цикле) одно такое утверждение. Затем необходимо для каждого пути в блок-схеме, ведущего из точки i с утверждением Аi в точку j с утверждение Аj при условии, что на пути из i в j нет промежуточных точек с утверждениями, доказать, что если мы находимся в точке i и справедливо утверждение Аi а затем переходим по нашему пути в точку j, то при попадании в эту точку будет справедливо утверждение Аj. Для формализации такого доказательства необходимо:

1) использовать некоторую формальную нотацию для записи утверждений;

2) формализовать то, что необходимо доказывать для каждого пути в блок-схеме;

3) использовать для выполнения доказательства некоторую формальную систему вывода (дедуктивную систему).

Мы рассмотрим лишь вопросы, относящиеся к п. 1 и 2. Для цели, указанной в п. 1, можно использовать нотацию исчисления предикатов (или другую формальную нотацию), с помощью которой можно формулировать нужные утверждения. Что касается п. 2, то надо дать некоторый систематический метод формирования для каждого из путей блок-схемы подлежащего доказательству формализованного высказывания. Множество всех таких высказываний, которые нужно доказывать для определения частичной правильности программы, иногда называют множеством условий верификации (verification conditions) для этой программы.

Для систематического формирования условий верификации некоторой блок-схемы поступим следующим образом. Рассмотрим по порядку все пути в блок-схеме и сформулируем алгоритм формирования условия верификации на пути из точки i в точку j.

1. Утверждение, относящееся к точке i, обозначим через Аi (Х, Y, ...), где
X,  Y, ...  – переменные, входящие в это утверждение. Аналогично обозначим и утверждение для точки j: Аj (Х, Y, ...). По пути из точки i в точку j значения переменных могут измениться (например, оператором присваивания). Для переменной V через epath (V) (изменение переменной вдоль пути) будем обозначать выражение, определяющее значение переменной V в точке j «в терминах» значений переменных в точке i и значений, присваиваемых переменным по мере прохождения пути. Если, например, на пути из i в j было три оператора присваивания 
                 Х ← X + 1,                Y ← Y + Y                и         X ← Х + Y – 2,

то  epath (Х) = (Х + 1) + (Y + Y) – 2 = X + 2•Y – 1,  epath (Y) = Y + Y = 2•Y.

2. На пути из точки i в точку j может встретиться несколько точек, где выполняются проверки. Будем обозначать такие проверки через tk (Х, Y, ...), где k – указывает точку, к которой относится проверка, а X, Y, ... – переменные, от которых она зависит. Предположим, что tk (Х, Y, ...), ..., t1 (Х, Y, ...) – полный набор всех проверок, встречающихся в различных точках на пути из точки i в точку j. Для каждой из этих проверок (tm (Х, Y, ...)) сформулируем высказывание:

,

если путь из i в j проходит по ветви, отмеченной T (истина), и

,

если путь из i в j проходит по ветви, отмеченной буквой F (ложь). Через path′ обозначается часть пути из i в j от точки i до точки m.

3. Образуем полное высказывание . Запишем формализованное условие верификации для пути из точки i в точку j:

[Аi (Х, Y, ...) Λ С path]  → Аj [e path (Х), e path (Y), ...).

Если на пути не встречаются проверки, то С path высказывание не включается.

Пример 5. Рассмотрим блок-схему (рис. 5.1), с которой мы уже имели дело в примере 4 и в учебных пособиях [1, 2]. Для записи утверждений, относящихся к разным точкам блок-схемы, использована нотация исчисления предикатов. Сформируем множество условий верификации.

1. Путь из точки 1 в точку 2 назовем р1. Для этого пути имеем

ер1 (J1) = J1,  ер1 (J2) = J2,

ер1 (IQ) = 0,  ер1 (IR) = J1.

Так как по пути проверки не выполняется, то можно написать следующее условие верификации для этого пути:

( 0 ≤ J1  Λ  1 ≤ J2 ) → [ер1 (J1) = ер1 (IQ) ● ер1 (J2) + ер1 (IR) Λ 0 ≤ ер1 (IR)],
( 0 ≤ J1  Λ  1 ≤ J2 ) → ( J1 = IQ ● J2 + J1 Λ  0 ≤ J1).

2. Путь из точки 2 через точки 3, 4 в точку 2 обозначим через р2.

Для этого пути имеем

ер2 (J1) = J1,  ер2 (J2) = J2,

ер2 (IQ) = IQ + 1, ер2 (IR) = IR – J2.

На пути есть только одна проверка IR < J2. Ту часть пути р2, которая ведет от точки 2 до этой проверки, обозначим через р2'. Так как путь р2 после проверки проходит по ветви, отмеченной F, то

.

Поскольку проверка только одна, получаем

Сp2 ≡ ¬ tp2.

Отсюда условие верификации для этого пути имеет вид

(J1 = IQ ● J2 + IR  Λ  0 ≤ IR  Λ J2 ≤ IR)→
→ [ер2 (J1) = ер2 (IQ) ● ер2 (J2) + ер2 (IR)  Λ  0 ≤ ер2 (IR)],

или после преобразования

(J1 = IQ ● J2 + IR Λ 0 ≤ IR Λ J2 ≤ IR) → [J1 = (IQ + 1) ● J2 + (IR – J2) Λ 0 < IR – J2].

3. Путь из точки 2 через 5 в точку 6 обозначим через рЗ.

Для этого пути имеем ер3 (J1) = J1, ер3 (J2) = J2, ер3 (IQ) = IQ, ер3 (IR) = IR. На пути встречается лишь одна проверка IR < J2.

Часть пути от точки 2 до этой проверки обозначим через р3'. Как и выше, имеем ер3' (IR) = IR и ер3' (J2) = J2. Так как после проверки путь проходит по ветви, обозначенной Т (истина), то

.

Следовательно, условие верификации для всего пути имеет вид

(J1 = IQ ● J2 + IR Λ 0 ≤ IR Λ IR < J2) → (J1 = IQ  ● J2 + IR Λ 0 < IR Λ IR < J2).

Для того, чтобы закончить формализованную версию доказательства правильности данной блок-схемы методом индуктивных утверждений, остается лишь доказать справедливость каждого из этих трех верификационных условий с помощью некоторой формальной системы вывода, которую обсуждать не будем.

Упражнения

1. Рассмотрите блок-схему, приведенную на рис. 5.2, сформулируйте и запишите индуктивные утверждения с помощью нотации исчисления предикатов и сформулируйте множество условий верификации.