Зададимся вопросом, что означает утверждение - программный элемент корректен? Наблюдения и рассуждения, отвечающие на это вопрос, могут показаться тривиальными. Но, как заметил один известный ученый, таковы все научные результаты, - они начинаются с обычных наблюдений и продолжаются путем простых рассуждений, но все это нужно делать упорно и настойчиво.
Предположим, некто пришел к вам с программой из 300 000 строк на С и спрашивает, корректна ли она? Если вы консультант, то взыщите высокую плату и ответьте - "нет". Вы, вероятно, окажетесь правы.
Для того чтобы можно было дать разумный ответ на подобный вопрос, одной программы недостаточно, необходима еще и ее спецификация, точно описывающая, что должна делать программа. Оператор
x:= y+1
сам по себе не является ни корректным, ни не корректным. Эти понятия приобретают смысл лишь по отношению к ожидаемому эффекту присваивания. Например, присваивание корректно по отношению к утверждению: "Переменные x и y имеют различные значения". Но не гарантируется его корректность по отношению к высказыванию: "переменная x отрицательна", поскольку результат присваивания зависит от значения y, которое может быть положительным.
Эти примеры иллюстрируют свойство, служащее отправной точкой в обсуждении проблемы корректности: программная система или ее элемент сами по себе ни корректны, ни не корректны. Корректность подразумевается лишь по отношению к некоторой спецификации. Строго говоря, мы и не будем обсуждать проблему корректности программных элементов, а лишь их согласованность (consistent) с заданной спецификацией. В наших обсуждениях мы будем продолжать использовать хорошо понимаемый термин "корректность", но всегда при этом помнить, что этот термин не применим к программному элементу, он имеет смысл лишь для пары - "программный элемент и его спецификация".
Свойство корректности ПО
Корректность - понятие относительное.
В этой лекции мы научимся выражать спецификации через утверждения (assertions), что поможет оценить корректность разработанного ПО.
Но пойдем дальше и перевернем проблему, - разработка спецификации является первым, важнейшим шагом на пути, гарантирующем, что ПО действительно соответствует спецификации. Существенную выгоду можно получить, когда спецификации пишутся одновременно с написанием программы, а лучше, до ее написания. Среди следствий такого подхода можно отметить следующее.