Математическая логика и теория алгоритмов [Г. И. Анкудинов] (pdf) читать постранично, страница - 8

пронесения кванторов через импликацию:
∀x[P(x) → Q(x)] → [∀x P(x) → ∀x Q(x)],
∀x[P(x) → Q(x)] → [∃x P(x) → ∃x Q(x)],

(2.7)
(2.8)

∀x[P(x) → Q] ↔ [∃x P(x) → Q].

(2.9)

Законы удаления
существования:

квантора

общности

и

введения

квантора

∀x P(x) → P(x),

(2.10)

P(x) → ∃x P(x).

(2.11)

Законы преобразования категорических высказываний:
∀x[P(x) → Q(x)] ↔ ⎤∃x[P(x) &⎤Q(x)],

(2.12)

∀x[P(x) → ⎤Q(x)] ↔ ⎤∃x[P(x) & Q(x)].

(2.13)

Все формулы исчисления предикатов можно разделить на три
типа:

• истинные при любой интерпретации, т.е. общезначимые;
• ложные при любой интерпретации, т.е. противоречивые;
• формулы, истинность которых зависит от интерпретации.
Чтобы определить тип формулы, то сначала следует попытаться
установить общезначимость или противоречивость заданной
формулы (тем более, что для одноместных предикатов это
алгоритмически разрешимая задача) и, если это не удается сделать,
то перейти к установлению значения истинности формулы для
заданной интерпретации, например так, как было показано выше в
примере 2.11.
Пример 2.12. Требуется установит тип формулы
∀x(⎤P(x) → ⎤Q(x)) ↔ ⎤∃x(⎤P(x) & Q(x)).
Попытаемся установить общезначимость или противоречивость данной
формулы. Для этого левую часть заданной эквивалентности заменим
равносильной формулой ∀x(P(x) \/ ⎤Q(x) на основе (1.38), а правую часть формулой ∀x⎤(⎤P(x) & Q(x)) на основе (2.2). Далее, с учетом (1.14), правая часть
примет вид ∀x(P(x) \/ ⎤Q(x)), т.е. исходная формула преобразована к виду

110

∀x(P(x) \/ ⎤Q(x)) ↔ ∀x(P(x) \/ ⎤Q(x)), где левая часть равна правой.
Следовательно, заданная формула является общезначимой.

2.6. Логика доказательства правильности
алгоритмов и программ
Цель данного раздела – познакомить читателя с принципами
верификации (доказательства правильности) алгоритмов и
программ. Создание и весь последующий жизненный цикл
надежного
программного
обеспечения
для
современных
информационно-вычислительных систем – многоэтапный и
трудоемкий процесс, который упрощенно можно охарактеризовать
как перевод требований технического задания сначала в точные
спецификации и, наконец, в текст программы.
Для описания алгоритмов используются различные методы,
отличающиеся
степенью
детализации
и
формализации.
Теоретическое описание обычно дается в повествовательноформальном изложении, цель которого – обосновать без лишних
подробностей процедуру, предлагаемую в качестве алгоритма. Для
наглядного
представления
структуры
алгоритмов
широко
применяются графические средства: графы, блок-схемы, сети.
Формальное и полное описание алгоритмов осуществляется на
алгоритмических языках; оно содержит всю необходимую для
реализации алгоритма информацию.
Сложность
программного
продукта
как
объекта
проектирования – основная причина ошибок перевода спецификаций
в текст программы и, следовательно, ненадежности программного
обеспечения. Для снижения сложности проекта используют
технологию
модульного
проектирования
и
объектноориентированный подход.
Распространенный подход к обеспечению надежности
проектируемого программного обеспечения – это тестирование.
Цель тестирования – выявление ошибок, вкравшихся в программу на

111

разных стадиях проектирования. При таком подходе при написании
программ акцент делается на их тестируемость, т.е. на создание
программ, которые удобно тестировать, а безошибочность и
корректность программы в значительной степени зависят от
творческих способностей и интуиции разработчика.
В отличие от интуитивного подхода, который мы
охарактеризовали выше, рассматриваемый далее подход трактует
программирование как точную математическую науку. Этот подход
основан на том, что спецификация программ выражается средствами
логики, причем связь программ с их спецификацией осуществляется
путем определения семантики программ также средствами логики
(алгоритмическая логика Хоара* ). Этот подход открывает путь к
верификации (доказательству правильности) алгоритмов и программ
средствами логики.
В основе верификации программ (алгоритмов) – анализ
действия программ (алгоритмов) над данными. Для каждого
исходного состояния данных X, для которого выполнение
завершается, результирующее состояние данных Y является
определенным. Это значение Y единственно для данного X, поэтому
множество всех упорядоченных пар (X,Y) определяет функцию,
которую будем называть программной функцией.
Мы будем использовать символьные вычисления, чтобы
получить аналитическое выражение программной функции для
исследуемой программы. Программную функцию f для простой
программы P обозначим через [P] и определим выражением
[P]={(X,Y)⎥ Y=f(X)},
где X - состояние поля данных до выполнения P,
Y - состояние поля данных после выполнения P,
{(X,Y) ⎥ Y=f(X)} - множество пар (X,Y), таких, что