ГОСТ Р НСО/МЭК 10746-4-2004
4.4.2.16 Введение (объекта)
См. создание (объекта), 4.4.2.15.
4.4.2.17 Удаление (<Х>)
Абстрактное представление удаления можно получить, если используется схема кадрирования.
Удаление можно смоделировать как осуществление операции по удалению состояния и идентифи
кации объекта из системы в целом.
Возможен случай, когда может быть смоделировано удаление на основе безактивносгн объекта.
Например, объект, связанное с которым будущее поведение не может быть осуществлено, так как
при этом будут нарушены инварианты, может рассматриваться в некотором смысле как удаленный.
Эта форма удаления не охватывается корректно определением, данным в ГОСТ Р ИСО/МЭК 10746-2,
так как оно не является разрушением объекта как таковым.
4.4.2.18 Экземпляр типа
Экземпляр типа ОРО представляется в Z элементом множества, члены которого удовлетворяют
предикату, т. е. типа ОРО. Для более специфического понятия типа, такого как тип шаблона,
экземпляр типа объекта или интерфейса соответствует инициализации текста на Z (или его расши
рения), представляющего рассматриваемый объект или интерфейс, такой, что для этого объекта или
интерфейса существует допустимое начальное состояние. Здесь схемой инициализации должны
удовлетворяться характеризующий предикат, заданный текстом спецификации, и ассоциированные
предикаты для возможных допустимых связываний (инвариантов).
Так как схема операции задает характеристики типа действия, то экземпляр типа действия
задается появлением этой или другой схемы операции, являющейся расширением данной, т. е.
расширение включает в себя характеризующие свойства типа действия.
4.4.2.19 Тип шаблона (<Х>)
В Z тип шаблона объекта или интерфейса является предикатом, который схема инициализации
сохраняет для объекта в допустимом состоянии 31 ассоциированных с ним интерфейсов. Таким
образом, все переменные состояния должны получить значения, а все необходимые предикаты
(инварианты) должны быть удовлетворены. Часто для проверки типа шаблона объекта или интер
фейса требуется проведение доказательства.
Тип шаблона действия соответствует предикату, устанавливающему, когда может появиться
шаблон действия, заданный схемой операции, т. е. реализация данной схемы операции. Таким образом,
все реализации должны удовтетворятъ предикатам для допустимых значений переменных, как
установлено в предикатах схемы операции.
4.4.2.20 Класс шаблонов (<Х>)
Класс шаблонов <Х> —это множество всех <Л>, которые явзяются экземплярами этого шаб
лона <Х>, где <Х> может быть объектом, интерфейсом или действием.
4.4.2.21 Производный класс/базовый класс
В Z для двух шаблонов А и В. где А —нарастающая модификация В и экземпляры А и В
находятся в отношении производный/базовый класс, нарастающие модификации В для создания А
могут включать в себя:
- добавление или удаление параметров состояния.
- добавтенне, удаление или изменение операций, или
- усиление или ослабление инвариантов.
4.4.2.22 Инвариант
Предикат, постоянная справедливость которого требуется спецификацией. Z позволяет запи
сывать инварианты непосредственно в схемах и аксиоматических описаниях. Часто инварианты
устанавливают ограничения на возможные значения, которые могут принимать переменные всхемах
зз аксиоматических описаниях. Если это так, то инвариант часто используется для ограничения
возможного поведения, заданного в спецификации.
4.4.2.23 Предусловие
Такое условие для состояния системы до осуществления операции, определенной схемой
операции. и на ее ввод, что существуют возможное состоязше после осуществления операции и вывод,
удовтетооряюшие постусловиям. Z позволяет записывать предусловия непосредственно.
4.4.2.24 Постусловие
Предикат, описывающий множество состояний, в которых может оказаться система после
осуществления операции, определенной схемой операции. Z позволяет записывать тх-тусювия не
посредственно.
25