 |
Спецификация для RemoveExtraBlanks.
|
|
|
|
Систематическое проектирование и корректность программ.
Методология проектирования программы и верификации корректности проекта может быть формализована. Спецификация для программы формулировки задачи и того, что программа должна делать играет центральную роль в такой формализации. Тщательный математический формализм играет роль даже в больших проектах, где невозможно достичь глубокой детализации.
Спецификации программ.
Спецификация программы описывает задачу и ее решение как отношение между входными и выходными строками.
Новые идеи: спецификация.
У каждой программы есть предназначение. Часто это предназначение решить какую-то задачу. Данные для решения задачи будут представлены в виде входной строки символов, а решение будет представлено в виде строки символов, которая является результатом выполнением программы.
Эти входные и выходные строки могут иметь слова и числа, которые значимы в контексте решения задачи, но читаются и записываются программой посимвольно как строки.
Программная спецификация задачи определяет набор входных строк которые представляют значимые для задачи данные и для каждой входной строки определяет набор (один или более) выходных строк которые являются приемлемым решением для данной формулировки задачи. Таким образом, спецификация – это отношение, состоящее из всех пар приемлемых экземпляров входных и выходных данных для решаемой задачи. Областью определения такого отношения являются все приемлемые наборы входных данных. Для строк, не принадлежащих области определения, не предусматривается соответствующего поведения программы.
|
|
|
Примеры:
Спецификация для сортировки строк символов. Вход – любая строка символов. Для каждой входной строки приемлема только одна выходная строка, а именно, строка с точно такими же элементами, но в сортированном порядке. Эта спецификация является функцией, потому что каждому входу соответствует единственный выход.
Спецификация для вычисления арифметического выражения с целыми числами. Большая часть строк символов не является приемлемыми входами, но только те, которые представляют арифметические выражения с целочисленными операндами. (Они могут быть точно описаны с помощью BNF.) Выходная строка должна быть представлена одним натуральным числом, которое является значением вычисленного входного выражения. За исключением того, что как результат будет представлен в выходной строке (система исчисления и т.д.) эта спецификация является функцией.
Спецификация для вычисления выражений описывающих множества символов. Входными данными будут только строки представляющие множества с явно перечисленными элементами. Выход должен представлять результат вычисления выражения. Выход может быть не уникальным, потому что элементы множества могут быть перечислены в различном порядке, то есть множество с двумя и более элементами может быть представлено более чем одной строкой символов. В этом случае спецификация – это отношение, которое не является функцией.
Эти три примера иллюстрируют, что спецификации программ могут быть функциями или отношениями и их области определения могут быть ограничены.
Хотя некоторые спецификации могут быть более применимыми, чем другие в данном контексте задачи, не существует жесткого правила для их разработки. Например, в спецификации про вычисление арифметических выражений может быть важным распознавать строки, которые не являются арифметическими выражениями и выдавать сообщения об ошибке. Каждый набор сообщений об ошибках для каждого отклонения синтаксиса арифметического выражения от корректного может быть частью спецификации. Таким образом, две спецификации для одних арифметических выражений, но с различной обработкой некорректного синтаксиса будут разными спецификациями. Спецификация может быть даже в форме «если синтаксис арифметического выражения некорректен, выдать сообщение об ошибке». Здесь программист свободен в выборе сообщений об ошибке. Здесь спецификация – это отношение, в котором каждое корректно сформулированное арифметическое выражение связано с уникальным выходом, а некорректно сформулированное выражение соответствует любому выходу, который может быть распознан как сообщение об ошибке. (Очевидно, что в данном случае неблагоразумно присваивать ошибкам номера и выдавать сообщение такие как, например 125, потому что они могут быть спутаны с результатами вычисления.)
|
|
|
Для задач, включающих сложные текстовые входные и выходные данные, полезно использовать BNF для описания области определения и значений в спецификации. Однако, часто с помощью BNF невозможно описать соответствие входных и выходных данных, что является существенной частью спецификации. Всякий раз, когда спецификация включает неформально описанные части, существует опасность двусмысленности. Например, спецификация для сортировки слов в тексте может описать строки области определения и области значений с использованием BNF. Но дополнительное выражение, что выходной текст должен содержать слова входного в сортированном порядке поднимает несколько вопросов. Должны ли повторяющиеся входные слова повторяться в выходном тексте или исключаться? Важно ли количество пробелов, разделяющее выходные слова? Порядок сортировки по возрастанию или по убыванию?
Не всегда желательно исключать двусмысленности из спецификации. Программные спецификации должны соответствовать решаемой задаче. Если выход будет использован другой программой, тогда точный формат позволит другой программой быть реализованной проще. Если выход будет использоваться человеком, тогда выход можно организовать более свободно в наиболее удобной из возможных форм.
|
|
|
Спецификация для 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)}
Спецификация программы – отношение, описывающее входы и допустимые выходы программы для данной задачи. Может оказаться трудным записать ее точно, но в любом случае это отношение с математической точки зрения. Спецификация сложной системы может состоять из сотен страниц текста, с инженерными рисунками, математическими формулами, описаниями из проблемной области, но это все равно отношение.
|
|
|
Корректность программ.
Формально, корректность программы – это свойство функции программы и отношения, которым задана спецификация, корректность может быть доказана с помощью теории множеств. Усилия должны быть разумно разделены между проектированием программы и доказательством ее корректности. Обычной ошибкой является слишком усложненный проект, который выходит из под интеллектуального контроля.
Отношение, задающее спецификацию, описывает, что программа должна делать. Оно выражает намерения, которые должны быть реализованы. Оно существует отдельно от любой программы, которая может быть написана, чтобы реализовать его. Фактически, спецификация является отправной точкой для программирования. Звучит привычно, что хорошо иметь спецификацию в уме до того как начать проектировать программу или разрабатывать стратегию проектирования.
С другой стороны, раз программа существует, ее функция определяет, что делает программа вне зависимости от намерений программиста при ее разработке. С использованием программного исчисления функция программы может быть вычислена из ее текста. Но ни спецификация, ни функция программы не описывают как именно программа выполняет свои действия. Но вычисление функции программы зависит от всех деталей внутренней работы программы.
Основной вопрос программирования и точно, основной вопрос программиста, пытающегося соответствовать спецификации, может быть сформулирован просто:
Для данных спецификации и программы, соответствует ли программа спецификации?
Неформально, если ответ на этот вопрос – «да», то говорят, что программа корректна в соответствии со спецификацией. Более формально, для данного отношения спецификации программы 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 корректна.
|
|
|
