Спецификации программ.

Систематическое проектирование и корректность программ.

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

Спецификации программ.

Спецификация программы описывает задачу и ее решение как отношение между входными и выходными строками.

Новые идеи: спецификация.

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

Эти входные и выходные строки могут иметь слова и числа, которые значимы в контексте решения задачи, но читаются и записываются программой посимвольно как строки.

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

Примеры:

Спецификация для сортировки строк символов. Вход – любая строка символов. Для каждой входной строки приемлема только одна выходная строка, а именно, строка с точно такими же элементами, но в сортированном порядке. Эта спецификация является функцией, потому что каждому входу соответствует единственный выход.

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

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

Эти три примера иллюстрируют, что спецификации программ могут быть функциями или отношениями и их области определения могут быть ограничены.

Хотя некоторые спецификации могут быть более применимыми, чем другие в данном контексте задачи, не существует жесткого правила для их разработки. Например, в спецификации про вычисление арифметических выражений может быть важным распознавать строки, которые не являются арифметическими выражениями и выдавать сообщения об ошибке. Каждый набор сообщений об ошибках для каждого отклонения синтаксиса арифметического выражения от корректного может быть частью спецификации. Таким образом, две спецификации для одних арифметических выражений, но с различной обработкой некорректного синтаксиса будут разными спецификациями. Спецификация может быть даже в форме «если синтаксис арифметического выражения некорректен, выдать сообщение об ошибке». Здесь программист свободен в выборе сообщений об ошибке. Здесь спецификация – это отношение, в котором каждое корректно сформулированное арифметическое выражение связано с уникальным выходом, а некорректно сформулированное выражение соответствует любому выходу, который может быть распознан как сообщение об ошибке. (Очевидно, что в данном случае неблагоразумно присваивать ошибкам номера и выдавать сообщение такие как, например 125, потому что они могут быть спутаны с результатами вычисления.)

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

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