Описание языка *****@***(стр. 1 )

Описание языка J@va

версия 1.4

Содержание

Содержание. 2

Введение. 7

Общие сведения о технологии тестирования UniTesK.. 9

Общие сведения о языке *****@***11

Специальные классы.. 11

Специальные операторы.. 11

Специальные ключевые слова. 12

Спецификации.. 14

Спецификационные классы.. 14

Назначение. 14

Описание. 14

Синтаксис. 15

Семантические ограничения. 15

Пример. 16

Инварианты данных. 17

Назначение. 17

Описание. 18

Синтаксис. 18

Семантические ограничения. 18

Пример. 18

Аксиомы.. 19

Назначение. 19

Описание. 19

Синтаксис. 20

Семантические ограничения. 20

Пример. 20

Эквивалентности. 21

Назначение. 21

Описание. 21

Синтаксис. 22

Семантические ограничения. 22

Пример. 23

Спецификационные методы.. 23

Назначение. 23

Описание. 23

Синтаксис. 24

Семантические ограничения. 25

Пример. 26

Описание возможных исключений. 26

Назначение. 26

Описание. 26

Синтаксис. 26

Семантические ограничения. 26

Пример. 26

Описание ограничений доступа. 27

Назначение. 27

Описание. 27

Синтаксис. 28

Семантические ограничения. 29

Пример. 29

Предусловие. 30

Назначение. 30

Описание. 30

Синтаксис. 30

Семантические ограничения. 30

Пример. 31

Постусловие. 31

Назначение. 31

Описание. 31

Синтаксис. 31

Семантические ограничения. 32

Пример. 32

Оператор branch. 33

Назначение. 33

Описание. 33

Синтаксис. 33

Семантические ограничения. 33

Пример. 34

Оператор mark. 34

Назначение. 34

Описание. 34

Синтаксис. 35

Семантические ограничения. 35

Пример. 35

Превыражения. 36

Назначение. 36

Описание. 36

Синтаксис. 36

Семантические ограничения. 37

Пример. 37

Группы спецификаций. 38

Назначение. 38

Описание. 38

Синтаксис. 38

Семантические ограничения. 38

Пример. 39

Описание тестового покрытия. 40

Покрытие ветвей функциональности. 40

Пример. 40

Покрытие помеченных путей. 41

Пример. 41

Покрытие предикатов. 42

Пример. 42

Покрытие дизъюнктов. 43

Пример. 43

Оператор coverage. 44

Назначение. 44

Описание. 44

Синтаксис. 45

Семантические ограничения. 46

Пример. 46

Модификатор irrelevant 47

Назначение. 47

Описание. 47

Синтаксис. 47

Семантические ограничения. 47

Пример. 47

Оператор tautology. 48

Назначение. 48

Описание. 48

Синтаксис. 48

Семантические ограничения. 48

Пример. 49

Связи между спецификациями.. 51

Наследование спецификационных классов. 51

Назначение. 51

Описание. 51

Синтаксис. 51

Семантические ограничения. 51

Пример. 52

Уточнение спецификационных классов. 54

Назначение. 54

Описание. 54

Синтаксис. 54

Семантические ограничения. 55

Пример. 55

Медиаторы... 60

Медиаторные классы.. 60

Назначение. 60

Описание. 60

Синтаксис. 60

Семантические ограничения. 61

Пример. 61

Реализационные ссылки. 62

Назначение. 62

Описание. 62

Синтаксис. 62

Семантические ограничения. 62

Пример. 63

Тестовые сценарии.. 64

Сценарные классы.. 64

Назначение. 64

Описание. 64

Синтаксис. 64

Семантические ограничения. 65

Пример. 65

Сценарные методы.. 66

Назначение. 66

Описание. 66

Синтаксис. 66

Семантические ограничения. 67

Пример. 67

Итерационные циклы.. 67

Назначение. 67

Описание. 67

Синтаксис. 68

Семантические ограничения. 69

Пример. 69

Комбинаторы выбора. 69

Назначение. 69

Описание. 69

Синтаксис. 70

Семантические ограничения. 70

Пример. 70

Комбинаторы сериализации. 71

Назначение. 71

Описание. 71

Синтаксис. 72

Семантические ограничения. 72

Пример. 72

Переменные обобщенного состояния. 72

Назначение. 72

Описание. 72

Синтаксис. 73

Семантические ограничения. 73

Пример. 73

Оператор stop. 73

Назначение. 73

Описание. 74

Синтаксис. 74

Семантические ограничения. 74

Пример. 75

Грамматика *****@***76

Введение

Данный документ представляет собой справочник по языку *****@***В нем содержится описание конструкций языка, их синтаксис, связанные с ними семантические ограничения и примеры их использования для разработки тестов.

Документ предназначен пользователям инструмента *****@***и входит в комплект документации, поставляемой с ним.

Документ состоит из следующих разделов:

Общие сведения о технологии тестирования UniTesK

В этом разделе приводятся общие сведения о технологии тестирования UniTesK, дается краткое описание архитектуры тестовой системы и связанная с технологией терминология.

Общие сведения о языке J@va

В этом разделе приводятся общие сведения о языке J@va, кратко описываются его дополнительные конструкции, операторы и ключевые слова.

Спецификации

В этом разделе описываются конструкции языка для написания спецификаций, то есть функциональных требований к тестируемой системе.

Описание тестового покрытия

В этом разделе описываются стандартные тестовые покрытия, поддерживаемые языком и конструкции языка для описания тестовых покрытий.

Связи между спецификациями

В этом разделе рассматриваются связи между спецификациями, которые бывают двух видов: наследование и уточнение. Описываются конструкции языка для задания этих видов связей.

Медиаторы

В этом разделе описываются конструкции языка для написания медиаторов, то есть компонентов тестовой системы, осуществляющих связь между спецификацией и тестируемой системой.

Тестовые сценарии

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

Грамматика J@va

В этом разделе приводится полное описание грамматики языка в форме БНФ (Бэкуса-Наура Форма).

В документе используются следующие шрифтовые и цветовые выделения:

Ключевые термины технологии тестирования UniTesK и языка J@va, встречаемые в разделе впервые, выделены курсивом. Например:

целевая система

Ссылки на разделы документа и внешние информационные ресурсы выделены синим подчеркнутым курсивом. Например:

Спецификационные классы

Примеры на языке *****@***выделены моноширинным шрифтом. При этом:

·  Ключевые слова языка Java – синим жирным шрифтом

·  Специальные ключевые слова языка *****@***– фиолетовым жирным шрифтом

·  Комментарии – серым цветом

Например:

// объявление пакета model

specification package model;

// объявление спецификационного класса SpecificationClass

public class SpecificationClass

{

...

}

Фрагменты кода, имена пакетов, классов, методов, полей, ключевые слова, операторы и элементы грамматики, встречаемые в тексте, выделены жирным шрифтом. Например:

java.lang.Throwable

Дополнительную информацию по инструменту *****@***и технологии тестирования UniTesK можно найти в следующих источниках:

Документ Установка и удаление J@T, входящий в комплект документации, поставляемой с *****@***Документ J@T. Быстрое знакомство, входящий в комплект документации, поставляемой с *****@***Документ J@T. Руководство пользователя, входящий в комплект документации, поставляемой с *****@***Сайт http://www.unitesk.com, посвященный технологии тестирования UniTesK По техническим вопросам, связанным с J@T, обращайтесь в службу поддержки инструмента по адресу: [e-mail]

Общие сведения о технологии тестирования UniTesK

Процесс тестирования должен демонстрировать, что целевая система (то есть система, для которой разрабатываются тесты) удовлетворяет требованиям, предъявляемым к ней, на некотором достаточно показательном наборе ситуаций. Для этой цели при разработке тестов необходимо иметь полное и точное описание требований к целевой системе. Дополнительно нужно определить набор тестовых ситуаций, на котором будет проводиться тестирование.

Технология тестирования UniTesK сфокусирована на функциональном тестировании, нацеленным на проверку соответствия целевой системы функциональным требованиям (то есть, требованиям, описывающим, что система должна делать). Одна из основных целей UniTesK – автоматизировать насколько это возможно процесс функционального тестирования.

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

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

Привязку спецификаций к целевой системе осуществляют специальные компоненты тестовой системы, называемые медиаторами.

Как описать достаточный набор тестовых ситуаций?

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

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

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

Когда есть описание функциональности целевой системы и значение метрики тестового покрытия, которое нужно достичь, остается единственная проблема – генерация тестовой последовательности (то есть последовательности обращений к операциям целевой системы) для достижения заданного тестового покрытия.

Описание тестовой последовательности называется тестовым сценарием.

Технология тестирования UniTesK предлагает специальную технику для описания тестовых сценариев, основанную на понятии конечных автоматов. Язык *****@***позволяет описывать автоматную модель целевой системы в компактной, удобной для повторного использования форме. По данному описанию автоматически строится обход графа состояний конечного автомата, в результате которого генерируется требуемая тестовая последовательность.

Общие сведения о языке J@va

Язык *****@***является расширением языка программирования Java и специально разработан для поддержки технологии тестирования UniTesK.

В нем есть специальные конструкции, которые позволяют компактным и удобным образом описывать функциональные требования к целевой системе и тестовые последовательности.

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

Специальные классы

В язык *****@***введены три специальных вида классов:

Спецификационные – описывающие функциональность целевой системы (см. раздел Спецификационные классы) Медиаторные – осуществляющие привязку спецификационных классов к компонентам целевой системы (см. раздел Медиаторные классы) Сценарные – описывающие тестовые последовательности для достижения определенных целей тестирования (см. раздел Сценарные классы)

Их объявления должны находится в файлах с расширением se_java.

В каждом таком файле должен располагаться ровно один специальный класс, причем его имя должно совпадать с именем файла. Этот класс входит в состав пакета, имя которого указывается в начале файла с использованием конструкции specification package <имя пакета>, например:

// объявление пакета model

specification package model;

Объявление пакета обязательно должно присутствовать в начале se_java файла, даже если это пакет без имени. В этом случае следует писать:

// объявление пакета без имени

specification package ;

За исключением способа объявления, пакеты в языке *****@***ничем не отличаются от пакетов в Java. Так же как и в Java, для импортирования класса, находящегося в другом пакете, используется конструкция import <полное имя класса>, а для импортирования всех классов одного пакета – import <имя пакета>.*, например:

// импортирование всех классов пакета model

import model.*;

Специальные операторы

В язык *****@***введены два дополнительных оператора:

·  Оператор импликации (оператор =>)

·  Оператор взятия презначения (оператор @) (см. раздел Превыражения)

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

Выражение x => y эквивалентно выражению !x || y, и при его вычислении, также как при вычислении других логических операторов, действуют правила короткой логики.

Оператор импликации ассоциативен справа налево, то есть выражение x => y => z эквивалентно выражению x => (y => z).

Специальные ключевые слова

В язык *****@***введены дополнительные ключевые слова, которые нельзя использовать в качестве идентификаторов:

alternative axiom branch branch_coverage choice complement coverage down disjunct_coverage equivalence implementation invariant irrelevant iterate mark mark_coverage mediator partition post pre predicate_coverage product reads recursive refines serialize scenario specification stable stop tautology thrown up updates writes

Спецификации

Спецификации представляют собой формальное описание функциональных требований к целевой системе в форме инвариантов данных, аксиом, эквивалентностей и спецификационных методов (см. разделы Инварианты данных, Аксиомы, Эквивалентности и Спецификационные методы соответственно).

Следуя концепии объектно-ориентированного программирования, реализованной в языке программирования Java, спецификации на языке J@va пишутся в виде набора спецификационных классов (см. раздел Спецификационные классы).

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

Привязка данных спецификационной модели к данным целевой системы и спецификационных методов к операциям целевой системы осуществляется при помощи медиаторов (см. раздел Медиаторы).

Спецификационные классы

Назначение

Спецификационные классы являются основными структурными единицами спецификации.

Обычно каждый спецификационный класс содержит описание требований к некоторому компоненту целевой системы.

Описание

Спецификационные классы оформляются как обычные классы Java и могут содержать следующие объявления:

·  Поля спецификационной модели данных (см. раздел Спецификации)

·  Инварианты данных (см. раздел Инварианты данных)

·  Аксиомы (см. раздел Аксиомы)

·  Эквивалентности (см. раздел Эквивалентности)

·  Спецификационные методы (см. раздел Спецификационные методы)

·  Группы спецификаций (см. раздел Группы спецификаций)

·  Обыкновенные методы (в частности, конструкторы), используемые для вспомогательных целей

Язык *****@***поддерживает наследование и уточнение спецификационных классов (см. разделы Наследование спецификационных классов и Уточнение спецификационных классов соответственно).

Синтаксис

SE_ClassDeclaration ::= ( ClassModifier )*

SE_UnmodifiedClassDeclaration

;

ClassModifier ::= "public" | "abstract" | "final" | "strictfp" ;

SE_UnmodifiedClassDeclaration ::= "class"

Identifier

( ( "extends" | "refines" ) ClassType )?

( "refines" SE_Refines ( "," SE_Refines )* )?

( Interfaces )?

SE_ClassBody

;

ClassType ::= TypeName ;

TypeName ::= Qualident ;

SE_Refines ::= ClassType "up" ClassType "down" ClassType ;

Interfaces ::= "implements" InterfaceType ( "," InterfaceType )* ;

SE_ClassBody ::= "{" ( SE_ClassBodyDeclaration )* "}" ;

SE_ClassBodyDeclaration ::= ClassBodyDeclaration

| SE_InvariantDeclaration

| SE_AxiomDeclaration

| SE_EquivalenceDeclaration

| SE_SpecificationBlock

| SE_MethodSpecification

;

Грамматику элементов SE_InvariantDeclaration, SE_AxiomDeclaration, SE_EquivalenceDeclaration, SE_SpecificationBlock и SE_MethodSpecification можно найти в разделах Инварианты данных, Аксиомы, Эквивалентности, Группы спецификаций и Спецификационные методы соответственно.

Семантические ограничения

Спецификационные классы могут наследовать или уточнять только спецификационные классы Спецификационные классы всегда наследуют библиотечный класс jatva.lang.ModelObjectForCheck, хотя это явно не указывается В спецификационном классе для каждого спецификационного метода SpecificationMethod автоматически генерируются следующие методы:

·  public synchronized [static] int testSutuationId_SpecificationMethod(…) – параметрами метода являются параметры спецификационного метода SpecificationMethod и дополнительный строковый параметр

·  public synchronized [static] boolean precondition_SpecificationMethod(…) – параметрами метода являются параметры спецификационного метода SpecificationMethod

Эти методы являются статическими тогда и только тогда, когда исходный спецификационный метод статический

Пример

// объявление пакета model

specification package model;

// объявление спецификационного класса AccountSpecification

public class AccountSpecification

{

// объявление полей спецификационной модели данных

static public int maximumCredit;

public int balance;

// объявление конструктора спецификационного

// класса AccountSpecification

public AccountSpecification()

{

}

// объявление инварианта данных I

invariant I()

{

return balance >= - maximumCredit;

}

// объявление спецификационного метода deposit

specification public void deposit(int sum)

// описание ограничений доступа

// спецификационного метода deposit

reads sum, // параметр sum и статическое поле

Integer. MAX_VALUE // MAX_VALUE класса Integer

// доступны только на чтение

updates balance // к полю balance возможен

// произвольный доступ

{

// предусловие спецификационного метода deposit

pre

{

return (0 < sum ) && (balance <= Integer. MAX_VALUE - sum);

}

// постусловие спецификационного метода deposit

post

{

branch "Single branch";

return balance == @balance + sum;

}

}

// объявление спецификационного метода withdraw

specification public int withdraw(int sum)

// описание ограничений доступа

// спецификационного метода withdraw

reads sum, // параметр sum и статическое поле

maximumCredit // maximumCredit доступны только на чтение

updates balance // к полю balance возможен

// произвольный доступ

{

// предусловие спецификационного метода withdraw

pre { return sum > 0; }

// постусловие спецификационного метода withdraw

post

{

if(balance < sum - maximumCredit)

{

branch "Withdrawn sum is too large";

return balance == @balance && withdraw == 0;

}

else

{

branch "Successful withdrawal";

return balance == @balance - sum && withdraw == sum;

}

}

}

}

Инварианты данных

Назначение

Инварианты данных предназначены для описания ограничений на значения полей спецификационной модели данных (см. раздел Спецификации).

С одной стороны, их можно рассматривать как ограничения подтипа, определяющие целостность спецификационной модели данных, с другой – как общие части пред- и постусловий всех спецификационных методов (см. раздел Спецификационные методы) спецификационного класса (см. раздел Спецификационные классы).

Описание

Инварианты данных могут объявляться только в спецификационных классах и представляются как методы без параметров, помеченные модификатором invariant и возвращающие значение типа boolean: true – если данные удовлетворяют ограничениям, false – иначе. Поскольку тип возвращаемого значения фиксирован, он не указывается.

Спецификационный класс может содержать несколько объявлений инвариантов данных, при этом проверяется конъюнкция задаваемых ими ограничений.

Инварианты данных могут быть статическими. Такие инварианты помечаются модификатором static и могут описывать ограничения только на статические поля спецификационной модели данных.

Синтаксис

SE_InvariantDeclaration ::= ( SE_InvariantModifier )*

"invariant"

Identifier

"("

")"

Block

;

SE_InvariantModifier ::= "static" ;

Семантические ограничения

Инварианты данных должны возвращать результат типа boolean Инварианты данных не должны иметь побочных эффектов, то есть не должны изменять состояние спецификационной модели данных Инварианты данных нельзя перегружать Инварианты данных нельзя вызывать явно (они вызываются тестовой системой автоматически при выполнения теста) Инварианты данных не должны выбрасывать исключения вовне

Пример

// объявление пакета model

specification package model;

// объявление спецификационного класса TimeSpecification

public class TimeSpecification

{

// объявление полей спецификационной модели данных

int hour;

int minute;

// объявление инварианта, описывающего ограничения

// на значения поля hour

invariant hours()

{

// часы могут изменяться в пределах от 0 до 23

return hour >= 0 && hour <= 23;

}

// объявление инварианта, описывающего ограничения

// на значения поля minute

invariant minutes()

{

// минуты могут изменяться в пределах от 0 до 59

return minute >= 0 && minute <= 59;

}

...

}

Аксиомы

Назначение

Аксиомы предназначены для описания ограничений на совместное поведение нескольких спецификационных методов (см. раздел Спецификационные методы).

Их используют в тех случаях, когда написать полную спецификацию в терминах инвариантов данных, эквивалентностей и спецификационных методов не представляется возможным или удобным (см. разделы Инварианты данных, Эквивалентности и Спецификационные методы соответственно).

Аксиомы – это наиболее общий способ спецификации, все остальные спецификационные конструкции могут быть заменены эквивалентными им аксиомами.

Описание

Аксиомы могут объявляться только в спецификационных классах (см. раздел Спецификационные классы) и представляются как методы, не имеющие параметров, помеченные модификатором axiom и возвращающие результат типа boolean. Поскольку тип возвращаемого значения фиксирован, он не указывается.

Аксиома может иметь предусловие, которое оформляется в виде отдельного блока, помеченного ключевым словом pre (см. раздел Предусловие).

Аксиомы используются для генерации сценарных методов (см. раздел Сценарные методы), поэтому в них можно использовать конструкции, используемые в для описания тестовой последовательности (см. раздел Тестовые сценарии), а именно:

Итерационные циклы (см. раздел Итерационные циклы) Комбинаторы выбора (см. раздел Комбинаторы выбора) Комбинаторы сериализации (см. раздел Комбинаторы сериализации) Переменные обобщенного состояния (см. раздел Переменные обобщенного состояния)

Аксиомы могут быть статическими. Такие аксиомы помечаются модификатором static и могут описывать ограничения на совместное поведение только статических спецификационных методов.

Синтаксис

SE_AxiomDeclaration ::= ( SE_AxiomModifier )*

"axiom"

Identifier

"("

")"

"{"

SE_PreBlock

"}"

;

SE_AxiomModifier ::= "static" ;

SE_PreBlock ::= ( BlockStatement )* ( SE_PreCondition ( BlockStatement )* )? ;

Грамматику элемента SE_PreCondition можно найти в разделе Предусловие.

Семантические ограничения

Аксиомы не должны иметь параметров и должны возвращать результат типа boolean Аксиомы нельзя перегружать В аксиомах нельзя использовать обращение к полям, объявленным в предках данного класса (через super) Все итерационные переменные аксиомы (см. раздел Итерационные циклы) должны иметь разные идентификаторы, отличающиеся от идентификаторов локальных переменных аксиомы В аксиомах между открывающейся фигурной скобкой и предусловием, если оно есть, нельзя использовать операторы return и throws

Пример

// объявление пакета model

specification package model;

// объявление спецификационного класса IntStackSpecification

public class IntStackSpecification

{

// объявление спецификационного метода push

specification public void push(int item)

// описание ограничений доступа спецификационного метода push

reads item // параметр item доступен только на чтение

updates this.? // к полям объекта возможен произвольный доступ

{...}

// объявление спецификационного метода pop

specification public int pop()

// описание ограничений доступа спецификационного метода pop

updates this.? // к полям объекта возможен произвольный доступ

{...}

// объявление аксиомы A

axiom A()

{

// итерационный цикл, перебирающий аргументы вызова метода push,

// проверка описанная в теле итерационного цикла будет выполняться

// для всех значений item от 0 до 9 в каждом обобщенном состоянии

iterate(int item = 0; item < 10; item++;)

{

push(item);

// результат метода pop должен совпадать с аргументом

// предшествующего вызова метода push

return pop() == item;

}

return true;

}

...

}

Эквивалентности

Назначение

Эквивалентности предназначены для описания утверждений о том, что эффекты от выполнения двух или более цепочек спецификационных методов (см. раздел Спецификационные методы) при одном и том же состоянии спецификационной модели данных (см. раздел Спецификации) тождественны. Под эффектом здесь понимается и возвращаемый результат, и итоговое состояние спецификационной модели данных.

Описание

Эквивалентности могут объявляться только в спецификационных классах (см. раздел Спецификационные классы) и представляются как методы, помеченные модификатором equivalence и имеющие сигнатуру, общую для всех цепочек, тождественность которых утверждается.

Эквивалентности могут иметь общее для цепочек предусловие, которое оформляется в виде отдельного блока, помеченного ключевым словом pre (см. раздел Предусловие).

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

У эквивалентностей должны описываться ограничения доступа (см. раздел Описание ограничений доступа), общие для всех ее цепочек.

Синтаксис

SE_EquivalenceDeclaration ::= "equivalence"

SE_MethodHeader

"{"

SE_PreBlock

"alternative" Block

( "alternative" Block )+

"}"

;

SE_PreBlock ::= ( BlockStatement )* ( SE_PreCondition ( BlockStatement )* )? ;

Грамматику элементов SE_MethodHeader и SE_PreCondition можно найти в разделах Спецификационные методы и Предусловие соответственно.

Семантические ограничения

Эквивалентности нельзя перегружать Каждый alternative блок должен подходить в качестве тела метода с указанной в объявлении эквивалентности сигнатурой

Внутри эквивалентностей можно использовать только локальные переменные и идентификаторы, на которые указан доступ в описании ограничений доступа

Перед предусловием эквивалентности, если оно присутствует, и после него, но до начала объявления alternative блоков, нельзя использовать операторы return и throws

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

·  В эквивалентности указан модификатор доступа reads, writes или updates, при этом во всех вызываемых методах описание ограничений доступа отсутствует

·  В эквивалентности указан модификатор доступа writes или updates, при этом у некоторых вызываемых методов указан модификатор доступа reads, у некоторых – описание ограничений доступа отсутствует

·  В эквивалентности указан модификатор доступа reads или updates, при этом у некоторых вызываемых методов указан модификатор доступа writes, у некоторых – описание ограничений доступа отсутствует

Пример

// объявление пакета model

specification package model;