Чтение онлайн

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

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

Синтаксически утверждения в нашей нотации будут обычными булевыми выражениями с небольшими расширениями. Одним из расширений является введение в нотацию термина "old", другим - введение символа ";" для обозначения конъюнкции (логического И). Вот пример:

Как между объявлениями и операторами, стоящими на разных строках, символ ";" является возможным, но не обязательным, так и в последовательности утверждений, записанных на разных строках, он может быть опущен, подразумеваясь по умолчанию. Эти соглашения облегчают идентификацию индивидуальных компонентов утверждения, которым обычно даются имена:

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

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

Этот пример даст возможность ознакомиться с практическим использованием утверждений. В предыдущей лекции была дана схема параметризованного класса "стек" в форме:

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

[x]. Программы remove и item применимы, только если число элементов стека не равно нулю.

[x]. put увеличивает, remove– уменьшает число элементов на единицу.

Такие свойства являются частью спецификации АТД, и даже люди далекие от использования любых формальных подходов неявно их понимают. Но в общих подходах к разработке ПО в программных текстах нельзя обнаружить следов спецификации. Предусловие и постусловие программы можно сделать явными элементами ПО. Так и поступим. Введем предусловие и постусловие как специальный вид объявлений с помощью ключевых слов require и ensure соответственно. Для класса "стек" это приведет к следующей записи, где временно оставлены пустые места для реализации:

Оба предложения require и ensure являются возможными; когда они присутствуют, то появляются в фиксированных местах, require– перед предложением local.

Обратите внимание на разделы feature, группирующие свойства по категориям, снабженных заголовками в виде комментариев. Категории Access, Status report, Element change - это несколько примеров из десятков стандартных категорий, используемых в библиотеках и применяемых повсеместно в примерах этой книги.

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

[x]. put не может быть вызвана, если стек заполнен;

[x]. remove и item не могут быть применены к пустому стеку.

Предусловия применяются ко всем вызовам программы, как внутри класса, так и у клиента. Корректная система никогда не вызовет программу в состоянии, в котором не выполняется ее предусловие.