Принцип обоснованности предусловия

Каждое предусловие программы при требовательном стиле проектирования должно удовлетворять следующим требованиям:

1 Предусловие появляется в официальной документации, поставляемой авторам клиентских модулей.

2 Предусловие формулируется только в терминах спецификации, что делает возможным его вычисление.

Первое требование поддерживается понятием краткой формы, изучаемой позднее в этой лекции. Второе требование исключает появление ограничений, определяемых реализацией поставщика программы. Например, для программы, занимающейся выталкиванием элементов из стека, предусловие not empty является требованием, проверяемым в терминах спецификации, и вытекающим из очевидного факта - из пустого стека ничего нельзя вытолкнуть. При вычислении квадратного корня предусловие x>0 отражает известный математический факт, - отрицательные числа не имеют вещественных квадратных корней.

Некоторые ограничения могут навязываться реализацией. Например, в программе put из класса STACK2 присутствие в качестве предусловия require not full связано с реализацией стека на основе массива. Но это не является нарушением принципа, поскольку класс STACK2 в полном соответствии с его спецификацией определяет стеки ограниченной емкости, что отражено, например, в предложении indexing этого класса. АТД, служащий в роли спецификации этого класса, не задает наиболее общий вид стеков, но является понятием стека ограниченной емкости.