Книга: Основы объектно-ориентированного программирования
О корректности ПО
О корректности ПО
Зададимся вопросом, что означает утверждение - программный элемент корректен? Наблюдения и рассуждения, отвечающие на это вопрос, могут показаться тривиальными. Но, как заметил один известный ученый, таковы все научные результаты, - они начинаются с обычных наблюдений и продолжаются путем простых рассуждений, но все это нужно делать упорно и настойчиво.
Предположим, некто пришел к вам с программой из 300 000 строк на С и спрашивает, корректна ли она? Если вы консультант, то взыщите высокую плату и ответьте - "нет". Вы, вероятно, окажетесь правы.
Для того чтобы можно было дать разумный ответ на подобный вопрос, одной программы недостаточно, необходима еще и ее спецификация, точно описывающая, что должна делать программа. Оператор
x:= y+1
сам по себе не является ни корректным, ни не корректным. Эти понятия приобретают смысл лишь по отношению к ожидаемому эффекту присваивания. Например, присваивание корректно по отношению к утверждению: "Переменные x и y имеют различные значения". Но не гарантируется его корректность по отношению к высказыванию: "переменная x отрицательна", поскольку результат присваивания зависит от значения y, которое может быть положительным.
Эти примеры иллюстрируют свойство, служащее отправной точкой в обсуждении проблемы корректности: программная система или ее элемент сами по себе ни корректны, ни не корректны. Корректность подразумевается лишь по отношению к некоторой спецификации. Строго говоря, мы и не будем обсуждать проблему корректности программных элементов, а лишь их согласованность (consistent) с заданной спецификацией. В наших обсуждениях мы будем продолжать использовать хорошо понимаемый термин "корректность", но всегда при этом помнить, что этот термин не применим к программному элементу, он имеет смысл лишь для пары - "программный элемент и его спецификация".
Свойство корректности ПО
Корректность - понятие относительное.
В этой лекции мы научимся выражать спецификации через утверждения (assertions), что поможет оценить корректность разработанного ПО. Но пойдем дальше и перевернем проблему, - разработка спецификации является первым, важнейшим шагом на пути, гарантирующем, что ПО действительно соответствует спецификации. Существенную выгоду можно получить, когда спецификации пишутся одновременно с написанием программы, а лучше, до ее написания. Среди следствий такого подхода можно отметить следующее.
[x]. Разработка ПО корректного с самого начала, проектируемого так, чтобы быть корректным. Один из создателей структурного программирования Харлан Д. Миллс в семидесятые годы написал статью со знаменательным названием "Как писать корректные программы и знать это". Слово "знать" в данном контексте означает снабжать программу в момент ее написания аргументами, характеризующими корректность.
[x]. Значительно лучшее понимание проблемы и достижение ее решения.
[x]. Упрощение задачи создания программной документации. Как будет позже показано, утверждения будут играть важную роль в ОО-подходе к документации.
[x]. Обеспечение основ для систематического тестирования и отладки.
Оставшаяся часть лекции посвящена исследованию этих вопросов. Одно предупреждение: языки программирования С, С++ и другие имеют оператор утверждения assert, динамически проверяющий истинность заданного утверждения в момент выполнения программы и останавливающий вычисление, если утверждение является ложным. Эта концепция, хотя и имеет отношение к предмету обсуждения, но является лишь малой частью использования утверждений в ОО-методе. Потому, если подобно многим разработчикам вы знакомы с этим оператором, не обобщайте ваше знание на всю картину, почти все концепции этой лекции, возможно, будут новыми.
- Базисные механизмы надежности
- О корректности ПО
- Выражение спецификаций
- Введение утверждений в программные тексты
- Предусловия и постусловия
- Контракты и надежность ПО
- Работа с утверждениями
- Инварианты класса
- Когда класс корректен?
- Связывание с АТД
- Инструкция утверждения
- Инварианты и варианты цикла
- Использование утверждений
- Обсуждение
- Ключевые концепции
- Библиографические замечания
- Упражнения
- Постскриптум: Катастрофа Ариан 5
- 11.2. СВОЙСТВА ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ
- Диагностика видеокарты
- Инварианты класса и семантика ссылок
- Использование утверждений
- Предостережение относительно использования приоритетов потоков и процессов
- Лекция 11. Проектирование по контракту: построение надежного ПО
- Обзор внешних факторов
- Ключевые вопросы
- Базисные механизмы надежности
- Формула корректности
- Ингредиенты доказательства корректности цикла
- Индикаторы корректности введенных данных