Корректность программ.

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

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

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

Основной вопрос программирования и точно, основной вопрос программиста, пытающегося соответствовать спецификации, может быть сформулирован просто:

Для данных спецификации и программы, соответствует ли программа спецификации?

Неформально, если ответ на этот вопрос – «да», то говорят, что программа корректна в соответствии со спецификацией. Более формально, для данного отношения спецификации программы r и программы P, мы говорим, что программа P корректна относительно r, если для каждого элемента x области определения r (экземпляра входных данных), P производит элемент области значений r, который соответствует x. То есть, для каждого входного x, P производит y, такой что < x, y> Î r.

Что выполняет P для входных данных, не принадлежащих области определения r несущественно, поскольку r определяет все поведение важное в контексте решения задачи. Это определение сводится к чисто теоретико-множественной идее, сформулированной в следующей теореме:

Теорема корректности. Программа P корректна относительно отношения спецификации r если и только если:

domain(r Ç P) = domain(r)

Доказательство:

Выражение r Ç P идентифицирует все приемлемые пары r, вычисляемые P. Следовательно, domain(r Ç P) идентифицирует множество входных данных, для которых P производит приемлемые выходные данные. Поскольку domain(r) – множество входных данных, для которых r определяет приемлемые выходные данные, условие

domain(r Ç P) = domain(r)

гарантирует, что P производит приемлемые выходные данные для каждого экземпляра входных данных, определяемых r. Что и требовалось доказать.

P может выполняться успешно для входных данных не заданных r, но такие пары P исключаются (r Ç P). Если P производит неприемлемые экземпляры выходных данных,

в (r Ç P) не существует элемента с соответствующими входными данными, и, следовательно, domain(r Ç P) не сможет быть равным domain(r).

Например, если:

r = {< A, †A†>, < B, †A†>, < A, †B†>, < B, †B†> }

и

P = {< x, Ñ x>: x - символ}

тогда

r Ç P = {< A, †A†>, < B, †B†> }

и

domain(r Ç P) = domain(r) = {A, B}

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

Следствие. Программа P корректна относительно функции спецификации f если и только если:

f Í P

Доказательство: Выражение f Ç P идентифицирует все приемлемые пары f вычисляемые P, которая должна быть f. То есть P корректна относительно f если и только если

f Ç P = f

Следовательно f Í P, что и требовалось доказать.

Рассмотрим корректность RemoveExtraBlanks, чья спецификация r приведена выше. Анализ программы в разделе 10.1.5 показал, что реально обработанные входные и выходные файлы описываются BNF правилами (с индексом P для программы):

1. < входной файл> _P:: = < файл 1> | < пробелы > < файл 1>

2. < файл 1>:: = < R> | < пробелы>

3. < R>:: = < слово> < пробелы> < R> | < слово> < пробелы>

4. < выходной файл> _P:: = < файл 2>

5. < файл 2>:: = S | < пустая строка >

6. < S>:: = < слово> < пробел> < S> | < слово>

элементы < слово> _S перемещенные из INPUT в OUTPUT те же самые. То есть,

P = {< < входной файл> _P, < выходной файл> _P>: words(< входной файл> _P) = words(< выходной файл> _P)}

Очевидно, что < выходной файл> _P и < выходной файл> _S идентичны, потому что идентичны < S> и < список слов>. < входной файл> _P и < входной файл> _S также идентичны, поскольку < R> описывает ту же строку что и < список-слов-пробелов> < пробелы>. Таким образом, спецификация и функция программы эквивалентны,

P = r,

и RemoveExtraBlanks корректна.