Препятствия на пути априорной схемы

Из-за простоты и ясности априорная схема, в принципе, идеальна. По трем причинам она не является универсально применимой:

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

Примером случая А1 является решатель линейных уравнений. Функция, дающая решение системы линейных уравнений в форме a x = b, где a - матрица, а x и b - векторы, может быть взята из соответствующего библиотечного класса MATRIX:

inverse (b: VECTOR): VECTOR

Решение системы находится так: x := a.inverse(b). Единственное решение системы существует, только если матрица не "сингулярна". (Сингулярность здесь означает линейную зависимость уравнений, признаком которой является равенство 0 определителя матрицы.) Можно было бы ввести проверку на сингулярность в предусловие inverse, требуя, чтобы вызовы клиента имели вид:

if a.singular then ...Подходящие действия для сингулярной матрицы... else x := a.inverse (b) end

Эта техника работает, но она неэффективна, поскольку определение сингулярности, по сути, дается тем же алгоритмом, что и нахождение решения системы. Так что одну и ту же работу придется выполнять дважды - сплошное расточительство.

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

Наконец, ограничение A3 возникает, когда невозможно проверить применимость операции без попытки выполнить ее, поскольку она взаимодействует с внешним миром - пользователем системы, линиями связи и так далее.

Содержание раздела