12.1.1. Спецификация для RemoveExtraBlanks.

Задача, решаемая RemoveExtraBlanks в раздле 10.1.3. была описана неформально. BNF для входа и выхода были разработаны как чать проекта. Добавляее индекс S для спецификации, получим:

1. <входной файл>_S ::= <список-слов-пробелов> <пробел >

| <пробелы> <список-слов-пробелов> <пробел>

2. <список-слов-пробелов> ::= <пустая строка> | <слово> <пробелы> <список-слов-пробелов>

3. <слово> ::= <НеПробел> | <слово>< НеПробел >

4. <пробелы > ::= <пробел> | <пробелы> <пробел>

5. <выходной файл>_S ::= <список слов> | <пустая строка>

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

CR. <Слова> в <списке слов> должно быть таким же и идти в том же порядке, что и в <списке-слов-пробелов>.

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

Один из способов сделать описание слов и их порядка более формальным – определить функцию, которая задает соответствие слов строки упорядоченному списку слов. Назовем эту функцию words.

Например:

words(†This is time is†) = <†This†, †is†, †time†, †is†>

Когда мы хотим обозначить все возможные строки определенные правилом BNF, мы используем имя правила, как например, мы говорим про <блок> в CF Pascal.

Тогда, входные данные для задачи удаления лишних пробелов <входной файл>_S, выходные данные <выходной файл>_S, связанные контекстным правилом

CR. words(<входной файл>_S) = words(<выходной файл>_S)

Эта спецификация может быть записана как

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

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

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

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

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

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

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

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

Неформально, если ответ на этот вопрос – «да», то говорят, что программа корректна в соответствии со спецификацией. Более формально, для данного отношения спецификации программы 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 корректна.