Нотация {P} A {Q} поможет выразить наше определение более строго.
Пусть C обозначает класс, Inv - инвариант, r - программа класса. Для каждой программы Bodyr - ее тело, prer(xr), postr(xr) - ее предусловие и постусловие с возможными аргументами xr. Если предусловие или постусловие для программы r опущены, то будем считать их заданными константой True.
Наконец, пусть DefaultC обозначает утверждение, выражающее тот факт, что атрибуты класса C имеют значения по умолчанию, определенные их типами. Например, DefaultSTACK2 для класса STACK2 является следующим утверждением:
representation = Void
capacity = 0
count = 0
Эта нотация позволяет дать общее определение корректности класса:
Определение: Корректность класса
Класс C корректен по отношению к своим утверждениям, если и только если:
1
Для любого правильного множества аргументов xp процедуры создания p:
{DefaultC and prep(xp)} Bodyp {postp(xp) and Inv}
2
Для каждой экспортируемой программы r и для любого множества правильных аргументов xr:
{prer(xr) and Inv} Bodyr {postr(xr) and Inv}
Это правило является математической формулировкой ранее рассмотренной неформальной диаграммы, показывающей жизненный цикл типичного объекта (рис. 11.4). Условие (1) означает, что любая процедура создания при ее вызове с выполняемым предусловием должна вырабатывать начальное состояние (S1 на рисунке), удовлетворяющее постусловию и инварианту. Условие (2) отражает тот факт, что любая экспортируемая процедура r (f и g на рисунке), вызываемая в состояниях (S1, S2, S3), удовлетворяющих предусловию и инварианту, должна завершаться в состояниях, удовлетворяющих постусловию и инварианту.
Два практических замечания:
[x]. Если у класса нет предложения creation, то можно полагать, что существует неявная процедура создания по умолчанию - nothing с пустым телом. Применение правила (1) к Bnothing в этом случае означает, что DefaultC влечет Inv; другими словами, значения полей по умолчанию должны удовлетворять инварианту в этом случае.
[x]. Из определения корректности класса следует, что любая экспортируемая программа может делать, все что угодно, если при ее вызове нарушается предусловие или инвариант.
Только что было описано, как определить корректность класса. На практике чаще хочется проверить, что данный класс действительно корректен. Эта проблема будет обсуждаться позднее в этой лекции.
Роль процедур создания
Инвариант класса задает множество свойств объектов (экземпляров класса), которые должны выполняться в стабильные времена жизни объектов. В частности, эти свойства должны выполняться сразу после создания экземпляра объекта.
Стандартный механизм распределения инициализирует поля значениями по умолчанию соответствующих типов, приписанных атрибутам. Эти значения могут удовлетворять или не удовлетворять инварианту. Если нет, то требуется специальная процедура создания, инициализирующая значения атрибутов таким образом, чтобы инвариант выполнялся. Поэтому процедуру создания можно рассматривать, как операцию, гарантирующую, что все экземпляры класса начинают жить, имея корректный статус, - в котором инвариант выполняется.
При первом представлении процедур создания они рассматривались, как способ ответа на земной (и очевидный) вопрос, как переопределить инициализацию по умолчанию, если она не подходит для моего класса. Другая рассматриваемая проблема, - как задать несколько различных механизмов инициализации. Но теперь, с введением инвариантов и теоретического обсуждения, отраженного в правиле (1), мы видим более весомую роль процедур создания. Теперь они создают уверенность, что любой экземпляр класса, только начиная жить, удовлетворяет фундаментальным правилам своей касты - инварианту класса.
Ревизия массивов
Набросок библиотечного класса ARRAY дан в предыдущей лекции. Теперь мы в состоянии дать ему подходящее определение. Фундаментальное понятие массива требует задания предусловий, постусловий и инварианта.
Приведем улучшенный, но все еще схематичный вариант, включающий утверждения. Предусловия выражают базисные требования к доступу и модификации элементов: индексы должны быть в допустимой области. Инвариант задает отношение, существующее между count, lower и upper. Компонент count разрешается реализовать функцией, а не задавать атрибутом.
indexing
description: "Последовательности значений одного типа или %
%согласованных типов, доступных по индексам - целым из заданного интервала %"
class ARRAY [G] creation
make
feature - Initialization (Инициализация)
make (minindex, maxindex: INTEGER) is
-- Создать массив с границами minindex и maxindex
-- (пустой если minindex > maxindex).
require
meaningful_bounds: maxindex >= minindex - 1
do
...
ensure
exact_bounds_if_non_empty: (maxindex >= minindex) implies
((lower = minindex) and (upper = maxindex))
conventions_if_empty: (maxindex < minindex) implies
((lower = 1) and (upper = 0))
end
feature -- Access (Доступ)
lower, upper, count: INTEGER
-- Минимальное и максимальное значение индекса; размер массива.
infix "@", item (i: INTEGER): G is
-- Элемент с индексом i
require
index_not_too_smalclass="underline" lower <= i
index_not_too_large: i <= upper
do ... end
feature -- Element change (Изменение элементов)
put (v: G; i: INTEGER) is
-- Присвоить v элементу с индексом i
require
index_not_too_smalclass="underline" lower <= i
index_not_too_large: i <= upper
do
...
ensure
element_replaced: item (i) = v