Партнерка на США и Канаду по недвижимости, выплаты в крипто
- 30% recurring commission
- Выплаты в USDT
- Вывод каждую неделю
- Комиссия до 5 лет за каждого referral
specification package model;
// импортирование вспомогательного класса ArrayList
import java. util. ArrayList;
// объявление спецификационного класса ListSpecification
public class ListSpecification
{
// объявление спецификационной модели данных
public ArrayList items;
// объявление спецификационного метода add,
// описывающего операцию, добавляющую элемент в список в i-ую позицию
specification public void add(Object obj, int i)
{
...
}
// объявление спецификационного метода get,
// описывающего операцию, возвращающую i-ый элемент списка
specification public Object get(int i)
{
...
}
// объявление спецификационного метода remove,
// описывающего операцию, удаляющую i-ый элемент списка и
// возвращающую удаленный элемент
specification public Object remove(int i)
{
...
}
// объявление спецификационного метода size,
// описывающего операцию, возвращающую размер списка
specification public int size()
{
...
}
}
Ниже приводится объявление спецификационного класса StringListSpecification, описывающего список строк и уточняющего спецификационный класс ListSpecification. В нем присутствуют и другие спецификационные методы, но они переиспользуют уже имеющиеся спецификации.
// объявление пакета model
specification package model;
// импортирование вспомогательного класса ArrayList
import java. util. ArrayList;
// объявление спецификационного класса StringListSpecification
public class StringListSpecification
// уточнение спецификационного класса ListSpecification
refines ListSpecification
up StringListToList
down ListToStringList
{
// объявление спецификационной модели данных
public ArrayList items;
// объявление инварианта данных AllItemsAreStrings, проверяющего,
// что все элементы списка являются строками
invariant AllItemsAreStrings()
{
for(int i = 0; i < items. size(); i++)
if(!(items. get(i) instanceof String))
return false;
return true;
}
// объявление спецификационных методов
specification public void add(String obj, int i)
refines StringListToList
{
post
{
branch "Single branch";
return true;
}
}
specification public void addFirst(String obj)
refines StringListToList
{
post
{
branch "Single branch";
return true;
}
}
specification public void addLast(String obj)
refines StringListToList
{
post
{
branch "Single branch";
return true;
}
}
specification public String get(int i)
refines StringListToList
{
post
{
branch "Single branch";
return true;
}
}
specification public String remove(int i)
refines StringListToList
{
post
{
branch "Single branch";
return true;
}
}
specification public int size()
refines StringListToList
{
post
{
branch "Single branch";
return true;
}
}
}
Ниже приводится объявление обобщающего медиатора StringListToList.
// объявление пакета model
specification package model;
// объявление обобщающего медиатора StringListToList
mediator public class StringListToList extends StringListSpecification
{
// объявление реализационной ссылки на объект
// спецификационного класса ListSpecification
implementation ListSpecification l;
// объявление медиаторных методов
public void add(String obj, int i)
{
l. add(obj, i);
}
public void addFirst(String obj)
{
l. add(obj, 0);
}
public void addLast(String obj)
{
l. add(obj, l. size());
}
public String get(int i)
{
return (String)l. get(i);
}
public String remove(int i)
{
return (String)l. remove(i);
}
public int size()
{
return l. size();
}
}
Ниже приводится объявление уточняющего медиатора ListToStringList.
// объявление пакета model
specification package model;
// импортирование вспомогательного класса ArrayList
import java. util. ArrayList;
// объявление уточняющего медиатора ListToStringList
mediator public class ListToStringList extends ListSpecification
{
// объявление реализационной ссылки на объект
// спецификационного класса StringListSpecification
implementation public StringListSpecification l;
// объявление медиаторных методов
public void add(Object obj, int i)
{
l. add((String)obj, i);
}
public Object get(int i)
{
return l. get(i);
}
public Object remove(int i)
{
return l. remove(i);
}
public int size()
{
return l. size();
}
// объявление метода синхронизации состояний
public void mapStateUp()
{
items = (ArrayList)l. items. clone();
}
}
Медиаторы
Медиаторы предназначены для связывания спецификации (см. раздел Спецификации) с целевой системой или со спецификацией другого уровня абстракции.
В дальнейшем для удобства изложения под целевой системой будем понимать либо непосредственно целевую систему, либо спецификацию другого уровня абстракции.
Медиаторы решают следующие задачи:
- Преобразование вызова спецификационного метода в обращение к операции целевой системы Преобразование результата выполнения операции целевой системы в результат спецификационного метода Построение спецификационной модели данных (см. раздел Спецификации) из состояния целевой системы
Медиаторные классы
Назначение
Медиаторные классы предназначены для реализации медиаторов.
Каждый медиаторный класс связывает спецификационный класс (см. раздел Спецификационные классы) с некоторым компонентом целевой системы или со спецификационным классом другого уровня абстракции.
Описание
Медиаторные классы помечаются модификатором mediator, который указывается в самом начале их объявления.
Медиаторные классы наследуются от спецификационных или медиаторных классов и перегружают все или часть спецификационных методов (см. раздел Спецификационные методы), реализуя описанное в них поведение через обращения к операциям целевой системы.
Методы медиаторного класса, перегружающие спецификационные методы, называются медиаторными методами.
При вызове у объекта медиаторного класса спецификационного метода, не перегруженного никаким медиаторным методом, будет выполнено тело спецификационного метода, если оно определено.
В медиаторном классе могут определяться поля, содержащие ссылки на объекты целевой системы. Такие поля помечаются модификатором implementation и называются реализационными ссылками (см. раздел Реализационные ссылки).
Синтаксис
"mediator" ClassDeclaration ;
Семантические ограничения
- Медиаторный класс может наследовать только спецификационный или медиаторный класс, причем какой-то класс он обязательно должен наследовать Каждый медиаторный класс Mediator имеет сгенерированный метод public static synchronized Mediator create(...), типы параметров которого есть типы всех нестатических реализационных ссылок данного класса и его предков в следующем порядке: ссылки предка перечисляются раньше, чем ссылки потомка, ссылки, описанные в одном классе перечисляются в порядке их объявления.
Пример
// объявление пакета model
specification package model;
// объявление спецификационного класса AccountSpecification
public class AccountSpecification
{
static public int maximumCredit;
public int balance;
// объявление спецификационного метода deposit
specification public void deposit(int sum)
reads sum, Integer. MAX_VALUE
updates balance
{
...
}
// объявление спецификационного метода withdraw
specification public int withdraw(int sum)
reads sum, maximumCredit
updates balance
{
...
}
...
}
Ниже приводится объявление медиаторного класса AccountMediator, наследующего спецификационный класс AccountSpecification и перегружающего спецификационные методы deposit и withdraw.
// объявление пакета model
specification package model;
// импортирование целевого класса Account
import target. Account;
// объявление медиаторного класса AccountMediator,
// наследующего спецификационный класс AccountSpecification
mediator public class AccountMediator extends AccountSpecification
{
// реализационная ссылка на целевой класс
implementation public Account target = new Account();
// объявление медиаторного метода deposit
public void deposit(int sum)
{
// вызов целевого метода deposit
target. deposit(sum);
}
// объявление медиаторного метода withdraw
public int withdraw(int sum)
{
// вызов целевого метода withdraw
return target. withdraw(sum);
}
// объявление метода синхронизаций состояний объектов
public void mapStateUp()
{
balance = target. balance;
}
// объявление метода синхронизаций состояний классов
public static void mapClassStateUp()
{
maximumCredit = target. maximumCredit;
}
}
Реализационные ссылки
Назначение
Реализационные ссылки являются специальными полями медиаторных классов (см. раздел Медиаторные классы) и предназначены для хранения ссылок на объекты целевой системы.
Реализационные ссылки используются для автоматической генерации статического метода create, создающего объект данного медиаторного класса (см. раздел Медиаторные классы).
Описание
Объявление реализационных ссылок отличается от объявления обычных полей добавлением в начало объявления модификатора implementation.
Синтаксис
"implementation" FieldDeclaration ;
Семантические ограничения
- Реализационные ссылки можно объявлять только в медиаторных классах Реализационные ссылки нельзя перегружать, то есть, не должно быть полей в предке и потомке с одинаковым именем, хотя бы одно из которых является реализационной ссылкой Реализационные ссылки должны иметь модификатор доступа только public или protected (они не могут иметь пакетный доступ или модификатор private) Инициализатор реализационной ссылки может быть только в медиаторном классе
Пример
// объявление пакета model
specification package model;
// импортирование целевого класса Queue
import target. Queue;
// объявление медиаторного класса QueueMediator,
// наследующего спецификационный класс QueueSpecification
mediator public class QueueMediator extends QueueSpecification
{
// объявление реализационной ссылки targetObject
// на объект целевого класса Queue
implementation public Queue targetObject = null;
...
}
Тестовые сценарии
Тестовые сценарии описывают тестовую последовательность (то есть последовательность обращений к операциям целевой системы), выполнение которой обеспечивает решение некоторой задачи тестирования.
Обычно в качестве такой задачи выступает тестирование некоторого набора операций целевой системы для достижения заданного уровня тестового покрытия (см. раздел Описание тестового покрытия).
Сценарные классы
Назначение
Сценарные классы предназначены для задания тестовых сценариев, то есть для описания тестовой последовательности, выполнение которой обеспечивает решение некоторой задачи тестирования.
Описание
Сценарные классы помечается модификатором scenario, который указывается в самом начале их объявления.
Внутри сценарных классов могут находиться объявления полей данных и методов.
Сценарные классы являются неявными наследниками класса jatva.lang.Scenario, который в свою очередь наследуется от java.lang.Thread, поэтому их можно использовать в качестве потоков: вызов метода start() в объекте сценарного класса запускает в отдельном потоке выполнение соответсвующего сценария.
В классе jatva.lang.Scenario определены следующие методы:
· jatva.lang.TestEngine testEngine() – возвращает обходчик данного сценарного объекта, то есть компонент тестовой системы, реализующий некоторый алгоритм генерации тестовой последовательности
· void setTestEngine(jatva.lang.TestEngine testEngine) – устанавливает обходчик данного сценарного объекта
· String getScenarioName() – возвращает имя сценарного класса, к которому относится данный объект
· jatva.lang.AbstractGenState getGenState() – создает и возвращает объект, идентифицирующий обобщенное состояние (тестовую ситуацию), используемое обходчиком для генерации тестовой последовательности (см. раздел Обобщенное состояние документа J@T. Руководство пользователя)
В сценарном классе могут объявляться сценарные методы (см. раздел Сценарные методы).
Синтаксис
"scenario" ClassDeclaration ;
Семантические ограничения
- Сценарные классы могут наследовать только сценарные классы Сценарные классы всегда наследуют класс jatva.lang.Scenario, хотя это явно не указывается
Пример
// объявление пакета model
specification package model;
// объявление спецификационного класса SqrtSpecification
public class SqrtSpecification
{
// объявление статического спецификационного метода sqrt,
// описывающего извлечение квадратного корня
specification public static double sqrt(double x)
reads x
{
}
}
Ниже приводится объявление сценарного класса SqrtScenario, использующего спецификационный класс SqrtSpecification.
// объявление пакета model
specification package model;
// объявление сценарного класса SqrtScenario
scenario public class SqrtScenario
{
public double largeNumber = 1.0e15D;
public int numberOfTrials = 5;
// объявление конструкора сценарного класса SqrtScenario
public SqrtScenario(int p_number)
{
SqrtSpecification. attachClassOracle();
numberOfTrials = p_number;
}
// объявление сценарного метода sqrt
scenario public boolean sqrt()
{
iterate(int i = 0; i < numberOfTrials; i++;)
{
choice
{
{ SqrtSpecification. sqrt(i/largeNumber/numberOfTrials); }
{ SqrtSpecification. sqrt(1+i*largeNumber/numberOfTrials); }
{ SqrtSpecification. sqrt(((1 << i)+1)* largeNumber); }
}
}
return true;
}
// объявление статического метода main, запускающего тест
public static void main(String args[])
{
SqrtScenario myscenario = new SqrtScenario(5);
// запускаем выполнение соответствующего теста в отдельном потоке
myscenario. start();
try
{
// ожидаем окончание выполнение теста
myscenario. join();
}
catch(InterruptedException error)
{
}
}
}
Сценарные методы
Назначение
Сценарные методы предназначены для описания набора обращений к целевой системе, которые необходимо осуществить в каждом обобщенном состоянии, достижимом во время тестирования (см. раздел Обобщенное состояние документа *****@***Руководство пользователя).
Они также могут производить проверку корректности поведения вызываемых операций целевой системы.
Описание
Сценарные методы представляются как методы сценарного класса, не имеющие параметров, помеченные модификатором scenario и возвращающие результат типа boolean: true – если проверка показывает, что целевая система ведет себя корректно, false – иначе.
В сценарных методах для описания набора обращений к целевой системе можно использовать следующие конструкции:
- Итерационных циклов (см. раздел Итерационные циклы) Комбинаторов выбора (см. раздел Комбинаторы выбора) Комбинаторов сериализации (см. раздел Комбинаторы сериализации) Переменных обобщенного состояния (см. раздел Переменные обобщенного состояния)
Синтаксис
“scenario” MethodDeclaration ;
Семантические ограничения
- Сценарные методы не могут иметь параметров и должны возвращать результат типа boolean Сценарные методы можно определять только в сценарных классах Сценарные методы нельзя вызывать Сценарный метод может быть перегружен только сценарным методом, сценарный метод может перегружать только сценарный метод и не может реализовывать методы, наследуемые от интерфейсов В сценарных методах сценарного класса нельзя использовать обращения к полям, объявленным в предках данного класса, через super
Пример
// объявление сценарного метода sqrt
scenario public boolean sqrt()
{
iterate(int i = 0; i < numberOfTrials; i++;)
{
choice
{
{ SqrtSpecification. sqrt(i/largeNumber/numberOfTrials); }
{ SqrtSpecification. sqrt(1+i*largeNumber/numberOfTrials); }
{ SqrtSpecification. sqrt(((1 << i)+1)* largeNumber); }
}
}
// дополнительных проверок не производится
return true;
}
Итерационные циклы
Назначение
Итерационные циклы предназначены для записи перебора значений параметров обращений к операциям целевой системы в сценарных методах (см. раздел Сценарные методы).
В аксиомах их можно рассматривать как типизированные кванторы всеобщности (см. раздел Аксиомы).
Описание
Синтаксис итерационного цикла языка *****@***похож на синтаксис цикла for(;;) языка Java. Объявление начинается с ключевого слова iterate, после которого в скобках через ; указаны:
- Объявление и инициализация итерационной переменной Условие продолжения итерации Шаг итерации Условие фильтрации
Все указанные части, за исключением первой, являются необязательными и могут быть опущены. Объявление заканчивается телом итерационного цикла – итерационным блоком. Несмотря на сходство в записи итерационного цикла и цикла for(;;), итерационные циклы всегда выполняются хотя бы один раз, если выполнено условие фильтрации.
Итерационный цикл:
iterate(<объявление и инициализация итерационной переменной>;
<условие продолжение итерации>;
<шаг итерации>;
<условие фильтрации>)
<итерационный блок>
подобен циклу:
<объявление и инициализация итерационной переменной>;
do
{
if(<условие фильтрации>)
<итерационный блок>;
<шаг итерации>;
}
while(<условие продолжение итерации>);
Итерационные переменные, то есть переменные, значения которых перебираются в итерационном цикле, не являются обычными переменными, значения которых теряются при выходе из сценарного метода. Их значения запоминаются в специальной структуре данных, связанной с текущим обобщенным состоянием (см. раздел Обобщенное состояние документа J@T. Руководство пользователя). Эти значения становятся доступными, как только тест перейдет в данное обобщенное состояние снова.
Итерационные переменные являются частным случаем переменных обобщенного состояния (см. раздел Переменные обобщенного состояния).
Для прекращения итерации используется оператор stop (см. раздел Оператор stop).
Синтаксис
SE_Iterate ::= "iterate"
"("
( "final" )?
Type
VariableDeclarator
";"
( Expression )?
";"
( ForUpdate )?
";"
( Expression )?
")"
Statement
;
Семантические ограничения
- Итерационные циклы могут использоваться только в сценарных методах и аксиомах Выражения, задающие условия продолжения итерации или условия фильтрации, если они присутствуют в итерационном цикле, должны иметь тип boolean Итерационная переменная должна быть инициализирована Итерационная переменная должна либо быть примитивного типа, либо иметь метод public Object clone()
Пример
// объявление сценарного класса AccountTestScenario
scenario public class AccountTestScenario
{
// объявление сценарного метода deposit
scenario public boolean deposit()
{
if(target. balance < 10)
{
// итерационный цикл, описывающий перебор трех вызовов:
// target. deposit(1), target. deposit(3) и target. deposit(5)
iterate(int i = 1; i < 6; i++; i % 2 == 1)
{
// вызов целевого метода deposit
target. deposit(i);
}
}
// дополнительных проверок не производится
return true;
}
...
}
Комбинаторы выбора
Назначение
Комбинаторы выбора предназначены для описания перебора цепочек инструкций из некоторого множества в сценарных методах или аксиомах (см. разделы Сценарные методы и Аксиомы соответственно).
Описание
Объявление комбинаторов выбора начинается с ключевого слова choice, после которого в фигурных скобках указывается список, возможно пустой, блоков, каждый из которых содержит некоторую цепочку инструкций.
Комбинатор выбора:
choice
{
{ <цепочка1> }
{ <цепочка2> }
}
эквивалентен следующему итератору:
iterate(int i = 0; i < 2; i++;)
{
switch(i)
{
case 0:
{ <цепочка1> }
break;
default:
{ <цепочка2> }
break;
}
}
Синтаксис
SE_Choice ::= "choice" "{" ( Block )* "}" ;
Семантические ограничения
- Комбинаторы выбора могут использоваться только в сценарных методах и аксиомах
Пример
// объявление сценарного класса AccountTestScenario
scenario public class AccountTestScenario
{
public AccountSpecification target;
// объявление сценарного метода deposit
scenario public boolean deposit()
{
if(target. balance < 10)
{
// комбинатор выбора, описывающего перебор двух вызовов:
// target. deposit(1) и target. deposit(5)
choice
{
{ target. deposit(1); }
{ target. deposit(5); }
}
}
// дополнительных проверок не производится
return true;
}
// объявление сценарного метода withdraw
scenario public boolean withdraw()
{
// комбинатор выбора, описывающего перебор двух вызовов:
// target. withdraw(1) и target. withdraw(5)
choice
{
{ target. withdraw(1); }
{ target. withdraw(5); }
}
// дополнительных проверок не производится
return true;
}
...
}
Комбинаторы сериализации
Назначение
Комбинаторы сериализации предназначены для описания перебора цепочек инструкций, составленных особым образом из заданного множества инструкций, а именно: все инструкции из данных цепочек перемешиваются всеми возможными способами, но так, чтобы сохранить порядок инструкций, взятой из одной цепочки.
Описание
Объявление комбинаторов сериализации начинается с ключевого слова serialize, после которого в фигурных скобках указывается список, возможно пустой, блоков, каждый из которых содержит некоторую цепочку операций.
Комбинатор сериализации:
serialize
{
{ <инструкция1>; <инструкция2>; }
{ <инструкция3>; <инструкция4>; }
}
эквивалентен следующему комбинатору выбора:
choice
{
{ <инструкция1>; <инструкция2>; <инструкция3>; <инструкция4>; }
{ <инструкция3>; <инструкция4>; <инструкция1>; <инструкция2>; }
{ <инструкция1>; <инструкция3>; <инструкция4>; <инструкция2>; }
{ <инструкция3>; <инструкция1>; <инструкция2>; <инструкция4>; }
{ <инструкция1>; <инструкция3>; <инструкция2>; <инструкция4>; }
{ <инструкция3>; <инструкция1>; <инструкция4>; <инструкция2>; }
}
Блок { <цепочка инструкций> } внутри цепочки комбинатора сериализации рассматривается как одна инструкция.
Комбинаторы сериализации можно использовать только в сценарных методах и аксиомах (см. разделы Сценарные методы и Аксиомы соответственно).
Синтаксис
SE_Serialize ::= "serialize" "{" ( Block )* "}" ;
Семантические ограничения
- Комбинаторы сериализации могут использоваться только в сценарных методах и аксиомах
Пример
// объявление сценарного метода addAndRemove
scenario public boolean addAndRemove()
{
// объявление комбинатора сериализации
serialize
{
// описание множества цепочек для сериализации
{ target. add(1); target. add(1); target. remove(1); }
{ target. remove(2); target. add(2); target. remove(2); }
}
// дополнительных проверок не производится
return true;
}
Переменные обобщенного состояния
Назначение
Переменные обобщенного состояния предназначены для хранения данных, связанных с обобщенным состоянием (см. раздел Обобщенное состояние документа J@T. Руководство пользователя). Их значения запоминаются в специальной структуре данных, связанной с текущим обобщенным состоянием, и становятся доступными, как только тест перейдет в него снова.
Описание
Объявление переменных обобщенного состояния начинается с модификатора stable, после которого следует объявление переменных.
Код вида:
<оператор1>;
stable int i;
<оператор2>;
эквивалентен следующему (см. разделы Итерационные циклы и Оператор stop):
<оператор1>;
iterate(int i;;;)
{
<оператор2>;
stop i;
}
Синтаксис
SE_StableVariableDeclarationStatement ::= "stable"
LocalVariableDeclarationStatement
;
LocalVariableDeclarationStatement ::= LocalVariableDeclaration ";" ;
LocalVariableDeclaration ::= ( "final" )?
Type
VariableDeclarator
( "," VariableDeclarator )*
;
Семантические ограничения
- Переменные состояния могут использоваться только в сценарных методах и в аксиомах Переменные обобщенного состояния должны либо быть примитивного типа, либо иметь метод public Object clone()
Пример
// объявление сценарного метода fibbonachi
scenario public boolean fibbonachi()
{
// объявление переменных обобщенного состояния
stable int f1 = 0;
stable int f2 = 1;
// итерационный цикл, генерирующий последовательность из
// первых десяти чисел Фиббоначи
iterate(int i = 1; i <= 10; i++;)
{
f2 = f2 + f1;
f1 = f2 – f1;
target. method(f1);
}
return true;
}
Оператор stop
Назначение
Операторы stop предназначены для прекращения итерации по итерационной переменной в итерационном цикле (см. раздел Итерационные циклы) или для окончания перебора в комбинаторах выбора и сериализации (см. разделы Комбинаторы выбора и Комбинаторы сериализации соответственно).
Описание
Операторы stop могут использоваться только внутри итерационных циклов, комбинаторов выбора и комбинаторов сериализации.
Если оператор stop используется внутри итерационного цикла, он может иметь необязательный параметр – имя итерационной переменной, по которой нужно прекратить итерацию. При отсутствии параметра берется итерационная переменная итерационного цикла непосредственно содержащего данный оператор.
Прекращение итерации не означает немедленный выход из итерационного цикла, а лишь указывает, что данный проход по нему – последний.
Оператор stop может иметь модификатор recursive, который помимо прочего означает прекращение итераций по итерационным переменным внешних итерационных циклов.
Итерационный цикл вида:
iterate(<задание итерации по переменной i>)
{
iterate(<задание итерации по переменной j>)
{
if(<логическое выражение>)
recursive stop j;
<оператор>;
}
}
эквивалентен следующему:
iterate(<задание итерации по переменной i>)
{
iterate((<задание итерации по переменной j>)
{
if(<логическое выражение>)
{
stop j;
stop i;
}
<оператор>;
}
}
Синтаксис
SE_Stop ::= ( SE_StopModifier )* "stop" ( Identifier )? ";" ;
SE_StopModifier ::= "recursive" ;
Семантические ограничения
- Операторы stop без параметра могут использоваться только внутри итерационных циклов, комбинаторов выбора и комбинаторов сериализации Операторы stop c параметром могут использоваться только внутри итерационных циклов, в которых объявлена итерационная переменная с указанным именем
Пример
// объявление сценарного метода deposit
scenario public boolean deposit()
{
// итерационный цикл, перебирающий значение параметра
// спецификационного метода deposit
iterate(int i = 0; i < 10; i++;)
{
// если достигнута цель тестирования, прекращаем итерацию
if(achieveCoverage())
stop i;
// вызов операции целевой системы
target. deposit(i);
}
// дополнительных проверок не производится
return true;
}
Грамматика J@va
Goal ::= CompilationUnit | SE_CompilationUnit ;
Literal ::= <IntegerLiteral>
| <FloatingPointLiteral>
| BooleanLiteral
| <CharacterLiteral>
| <StringLiteral>
| NullLiteral
;
BooleanLiteral ::= "true" | "false" ;
NullLiteral ::= "null" ;
Type ::= PrimitiveType | ReferenceType ;
PrimitiveType ::= NumericType | "boolean" ;
NumericType ::= IntegralType | FloatingPointType ;
IntegralType ::= "byte" | "short" | "int" | "long" | "char" ;
FloatingPointType ::= "float" | "double" ;
ReferenceType ::= ClassOrInterfaceType | ArrayType ;
ClassOrInterfaceType ::= ClassType | InterfaceType ;
ClassType ::= TypeName ;
InterfaceType ::= TypeName ;
ArrayType ::= ( PrimitiveType | ClassOrInterfaceType ) ( Dim )+ ;
Identifier ::= <ID> ;
Qualident ::= Identifier ( "." Identifier )* ;
PackageName ::= Qualident ;
TypeName ::= Qualident ;
ExpressionName ::= Qualident ;
MethodName ::= Qualident ;
PackageOrTypeName ::= Qualident ;
ClassName ::= ClassOrInterfaceType ;
CompilationUnit ::= ( "package" PackageName ";" )?
( ImportDeclaration )*
( TypeDeclaration )*
;
SE_CompilationUnit ::= "specification"
"package"
( PackageName )?
";"
( SE_ImportDeclaration )*
( SE_TypeDeclaration )*
;
ImportDeclaration ::= SingleTypeImportDeclaration
| TypeImportOnDemandDeclaration
;
SingleTypeImportDeclaration ::= "import" TypeName ";" ;
TypeImportOnDemandDeclaration ::= "import" PackageOrTypeName "." "*" ";" ;
SE_ImportDeclaration ::= ImportDeclaration
| SE_SingleTypeImportDeclaration
| SE_TypeImportOnDemandDeclaration
;
SE_SingleTypeImportDeclaration ::= "import" "specification" TypeName ";" ;
SE_TypeImportOnDemandDeclaration ::= "import"
"specification"
PackageOrTypeName
"."
"*"
";"
;
TypeDeclaration ::= ClassDeclaration | InterfaceDeclaration | ";" ;
SE_TypeDeclaration ::= SE_ClassDeclaration
| ( "mediator" | "scenario" ) ClassDeclaration
| ";"
;
ClassDeclaration ::= ( ClassModifier )* UnmodifiedClassDeclaration ;
SE_ClassDeclaration ::= ( ClassModifier )* SE_UnmodifiedClassDeclaration ;
UnmodifiedClassDeclaration ::= "class"
Identifier
( "extends" ClassType )?
( Interfaces )?
ClassBody
;
SE_UnmodifiedClassDeclaration ::= "class"
Identifier
( ( "extends" | "refines" ) ClassType )?
( "refines" SE_Refines ( "," SE_Refines )* )?
( Interfaces )?
SE_ClassBody
;
ClassModifier ::= "public" | "abstract" | "final" | "strictfp" ;
SE_Refines ::= ClassType "up" ClassType "down" ClassType ;
Interfaces ::= "implements" InterfaceType ( "," InterfaceType )* ;
ClassBody ::= "{" ( ClassBodyDeclaration )* "}" ;
SE_ClassBody ::= "{" ( SE_ClassBodyDeclaration )* "}" ;
ClassBodyDeclaration ::= ClassMemberDeclaration
| ( "implementation" )? InstanceInitializer
| StaticInitializer
| ConstructorDeclaration
| ";"
;
SE_ClassBodyDeclaration ::= ClassBodyDeclaration
| SE_InvariantDeclaration
| SE_AxiomDeclaration
| SE_EquivalenceDeclaration
| SE_SpecificationBlock
| SE_MethodSpecification
;
ClassMemberDeclaration ::= ( "implementation")?
FieldDeclaration
| ( "scenario" )? MethodDeclaration
| MemberClassDeclaration
| MemberInterfaceDeclaration
;
FieldDeclaration ::= ( FieldModifier )*
Type
VariableDeclarator
( "," VariableDeclarator )*
";"
;
FieldModifier ::= "public"
| "protected"
| "private"
| "static"
| "final"
| "transient"
| "volatile"
;
VariableDeclarator ::= VariableDeclaratorId ( "=" VariableInitializer )? ;
VariableDeclaratorId ::= Identifier ( Dim )* ;
VariableInitializer ::= Expression | ArrayInitializer ;
MethodDeclaration ::= MethodHeader MethodBody ;
MethodHeader ::= ( MethodModifier )* ResultType MethodDeclarator ( Throws )?
( SE_AccessDescription )*
;
MethodModifier ::= "public"
| "protected"
| "private"
| "abstract"
| "static"
| "final"
| "synchronized"
| "native"
| "strictfp"
;
ResultType ::= Type | "void" ;
MethodDeclarator ::= Identifier
"("
( FormalParameter ( "," FormalParameter )* )?
")"
( Dim )*
;
FormalParameter ::= ( "final" )? Type VariableDeclaratorId ;
Throws ::= "throws" ClassType ( "," ClassType )* ;
MethodBody ::= Block | ";" ;
MemberClassDeclaration ::= ( MemberClassModifier )* UnmodifiedClassDeclaration ;
MemberClassModifier ::= "public"
| "protected"
| "private"
| "abstract"
| "static"
| "final"
| "strictfp"
;
MemberInterfaceDeclaration ::= ( MemberInterfaceModifier )*
UnmodifiedInterfaceDeclaration
;
MemberInterfaceModifier ::= "public"
| "protected"
| "private"
| "abstract"
| "static"
| "strictfp"
;
InstanceInitializer ::= Block ;
StaticInitializer ::= "static" Block ;
ConstructorDeclaration ::= ( ConstructorModifier )*
ConstructorDeclarator
( Throws )?
ConstructorBody
;
ConstructorModifier ::= "public" | "protected" | "private" ;
ConstructorDeclarator ::= Identifier
"("
( FormalParameter ( "," FormalParameter )* )?
")"
;
ConstructorBody ::= "{"
( ExplicitConstructorInvocation )?
( BlockStatement )*
"}"
;
ExplicitConstructorInvocation ::= ( "this" | ( Primary "." )? "super" )
"("
( ArgumentList )?
")"
";"
;
SE_InvariantDeclaration ::= ( SE_InvariantModifier )*
"invariant"
Identifier
"("
")"
Block
;
SE_InvariantModifier ::= "static" ;
SE_AxiomDeclaration ::= ( SE_AxiomModifier )*
"axiom"
Identifier
"("
")"
"{"
SE_PreBlock
"}"
;
SE_AxiomModifier ::= "static" ;
SE_EquivalenceDeclaration ::= "equivalence"
SE_MethodHeader
"{"
SE_PreBlock
"alternative" Block
( "alternative" Block )+
"}"
;
SE_SpecificationBlock ::= "specification"
( SE_AccessDescription )*
"{"
SE_PreBlock
( SE_MethodSpecification )+
"}"
;
SE_MethodSpecification ::= "specification"
SE_MethodHeader
"{"
SE_PreBlock
SE_PostCondition
( BlockStatement )*
"}"
;
SE_MethodHeader ::= MethodHeader
( "refines" SE_Refined ( "," SE_Refined )* )?
;
SE_Refined ::= ClassType | "super" ;
SE_AccessDescription ::= SE_AccessModifier SE_Access ( "," SE_Access )* ;
SE_AccessModifier ::= "reads" | "writes" | "updates" ;
SE_Access ::= ( ( Primary
| ExpressionName
| ( ClassName "." )? "super"
)
"."
)?
( Identifier | "?" | "*" )
| ArrayAccess
;
InterfaceDeclaration ::= ( InterfaceModifier )* UnmodifiedInterfaceDeclaration ;
UnmodifiedInterfaceDeclaration ::= "interface"
Identifier
( ExtendsInterfaces )?
InterfaceBody
;
InterfaceModifier ::= "public" | "abstract" | "strictfp" ;
ExtendsInterfaces ::= "extends" InterfaceType ( "," InterfaceType )* ;
InterfaceBody ::= "{" ( InterfaceMemberDeclaration )* "}" ;
InterfaceMemberDeclaration ::= ConstantDeclaration
| AbstractMethodDeclaration
| MemberClassDeclaration
| MemberInterfaceDeclaration
| ";"
;
ConstantDeclaration ::= ( ConstantModifier )*
Type
VariableDeclarator
( "," VariableDeclarator )*
";"
;
ConstantModifier ::= "public" | "static" | "final" ;
AbstractMethodDeclaration ::= ( AbstractMethodModifier )*
ResultType
MethodDeclarator
( Throws )?
";"
;
AbstractMethodModifier ::= "public" | "abstract" ;
ArrayInitializer ::= "{"
( VariableInitializer ( "," VariableInitializer )* )?
( "," )?
"}"
;
SE_PreBlock ::= ( BlockStatement )* ( SE_PreCondition ( BlockStatement )* )? ;
SE_PreCondition ::= "pre" Block ;
SE_PostCondition ::= "post" Block ;
Block ::= "{" ( BlockStatement )* "}" ;
BlockStatement ::= LocalVariableDeclarationStatement
| SE_StableVariableDeclarationStatement
| LocalClassDeclaration
| Statement
;
LocalClassDeclaration ::= ( LocalClassModifier )* UnmodifiedClassDeclaration ;
LocalClassModifier ::= "abstract" | "final" | "strictfp" ;
LocalVariableDeclarationStatement ::= LocalVariableDeclaration ";" ;
SE_StableVariableDeclarationStatement ::= "stable"
LocalVariableDeclarationStatement
;
LocalVariableDeclaration ::= ( "final" )?
Type
VariableDeclarator
( "," VariableDeclarator )*
;
Statement ::= LabeledStatement
| IfStatement
| WhileStatement
| ForStatement
| Block
| EmptyStatement
| ExpressionStatement
| SwitchStatement
| DoStatement
| BreakStatement
| ContinueStatement
| ReturnStatement
| SynchronizedStatement
| ThrowStatement
| TryStatement
| SE_Iterate
| SE_Serialize
| SE_Choice
| SE_Stop
| SE_Coverage
| SE_Tautology
| SE_BranchStatement
| SE_MarkStatement
| SE_IrrelevantStatement
;
SE_Iterate ::= "iterate"
"("
( "final" )?
Type
VariableDeclarator
";"
( Expression )?
";"
( ForUpdate )?
";"
( Expression )?
")"
Statement
;
SE_Serialize ::= "serialize" "{" ( Block )* "}" ;
SE_Choice ::= "choice" "{" ( Block )* "}" ;
SE_Stop ::= ( SE_StopModifier )* "stop" ( Identifier )? ";" ;
SE_StopModifier ::= "recursive" ;
SE_Coverage ::= "coverage" Identifier "=" SE_SubCoverageList ";" ;
SE_SubCoverageList ::= SE_SubCoverage ( "," SE_SubCoverage )* ;
SE_SubCoverage ::= "branch_coverage"
| "mark_coverage"
| "predicate_coverage"
| "disjunct_coverage"
| Expression
| "product" "(" SE_SubCoverageList ";" SE_SubCoverageList ")"
| "partition" "(" SE_SubCoverageList ")"
| "complement" "(" SE_SubCoverageList ")"
;
SE_Tautology ::= "tautology" Expression ";" ;
SE_BranchStatement ::= "branch" <StringLiteral> ";" ;
SE_MarkStatement ::= "mark" <StringLiteral> ";" ;
SE_IrrelevantStatement ::= "irrelevant" Statement ;
EmptyStatement ::= ";" ;
LabeledStatement ::= Identifier ":" Statement ;
ExpressionStatement ::= StatementExpression ";" ;
StatementExpression ::= Assignment
| PreIncrementExpression
| PreDecrementExpression
| PostIncrementExpression
| PostDecrementExpression
| MethodInvocation
| ClassInstanceCreationExpression
;
IfStatement ::= "if" "(" Expression ")" Statement ( "else" Statement )? ;
SwitchStatement ::= "switch" "(" Expression ")" SwitchBlock ;
SwitchBlock ::= "{" ( SwitchBlockStatementGroup )* ( SwitchLabel )* "}" ;
SwitchBlockStatementGroup ::= ( SwitchLabel )+ ( BlockStatement )+ ;
SwitchLabel ::= "case" ConstantExpression ":" | "default" ":" ;
WhileStatement ::= "while" "(" Expression ")" Statement ;
DoStatement ::= "do" Statement "while" "(" Expression ")" ";" ;
ForStatement ::= "for"
"("
( ForInit )?
";"
( Expression )?
";"
( ForUpdate )?
")"
Statement
;
ForInit ::= StatementExpression ( "," StatementExpression )*
| LocalVariableDeclaration
;
ForUpdate ::= StatementExpression ( "," StatementExpression )* ;
BreakStatement ::= "break" ( Identifier )? ";" ;
ContinueStatement ::= "continue" ( Identifier )? ";" ;
ReturnStatement ::= "return" ( Expression )? ";" ;
ThrowStatement ::= "throw" Expression ";" ;
SynchronizedStatement ::= "synchronized" "(" Expression ")" Block ;
TryStatement ::= "try" Block ( CatchClause )+
| "try" Block ( CatchClause )* Finally
;
CatchClause ::= "catch" "(" FormalParameter ")" Block ;
Finally ::= "finally" Block ;
Primary ::= PrimaryNoNewArray | ArrayCreationExpression ;
PrimaryNoNewArray ::= Literal
| Type "." "class"
| "void" "." "class"
| "this"
| ClassName "." "this"
| "(" Expression ")"
| ClassInstanceCreationExpression
| FieldAccess
| MethodInvocation
| ArrayAccess
| "thrown"
| "super" "." "pre"
;
ClassInstanceCreationExpression ::= ( "new" ClassOrInterfaceType
| Primary "." "new" Identifier
)
"("
( ArgumentList )?
")"
( ClassBody )?
;
Argument ::= Expression ;
ArgumentList ::= Argument ( "," Argument )* ;
ArrayCreationExpression ::= "new"
( ( PrimitiveType | TypeName )
( DimExpr )+
( Dim )*
| ArrayType ArrayInitializer
)
;
DimExpr ::= "[" Expression "]" ;
Dim ::= "[" "]" ;
FieldAccess ::= ( Primary | ( ClassName "." )? "super" ) "." Identifier ;
MethodInvocation ::= ( MethodName
| Primary "." Identifier
| "super" "." Identifier
| ClassName "." "super" "." Identifier
)
"("
( ArgumentList )?
")"
;
ArrayAccess ::= ( ExpressionName | PrimaryNoNewArray ) "[" Expression "]" ;
PostfixExpression ::= Primary
| ExpressionName
| PostIncrementExpression
| PostDecrementExpression
;
PostIncrementExpression ::= PostfixExpression "++" ;
PostDecrementExpression ::= PostfixExpression "--" ;
UnaryExpression ::= PreIncrementExpression
| PreDecrementExpression
| "+" UnaryExpression
| "-" UnaryExpression
| UnaryExpressionNotPlusMinus
;
PreIncrementExpression ::= "++" UnaryExpression ;
PreDecrementExpression ::= "--" UnaryExpression ;
UnaryExpressionNotPlusMinus ::= PostfixExpression
| "~" UnaryExpression
| "!" UnaryExpression
| CastExpression
| "@" UnaryExpression
;
CastExpression ::= "(" PrimitiveType ( Dim )* ")" UnaryExpression
| "(" ReferenceType ")" UnaryExpressionNotPlusMinus
;
MultiplicativeExpression ::= UnaryExpression
( ( "*" | "/" | "%" ) UnaryExpression )*
;
AdditiveExpression ::= MultiplicativeExpression
( ( "+" | "-" ) MultiplicativeExpression )*
;
ShiftExpression ::= AdditiveExpression
( ( "<<" | ">>" | ">>>" ) AdditiveExpression )*
;
RelationalExpression ::= ShiftExpression
( ( "<" | ">" | "<=" | ">=" ) ShiftExpression
| "instanceof" ReferenceType
)*
;
EqualityExpression ::= RelationalExpression
( ( "==" | "!=" ) RelationalExpression )*
;
AndExpression ::= EqualityExpression ( "&" EqualityExpression )* ;
ExclusiveOrExpression ::= AndExpression ( "^" AndExpression )* ;
InclusiveOrExpression ::= ExclusiveOrExpression ( "|" ExclusiveOrExpression )* ;
ConditionalAndExpression ::= InclusiveOrExpression
( "&&" InclusiveOrExpression )*
;
ConditionalOrExpression ::= ConditionalAndExpression
( "||" ConditionalAndExpression )*
;
SE_ImplicationExpression ::= ConditionalOrExpression
( "=>" ConditionalOrExpression )*
;
ConditionalExpression ::= SE_ImplicationExpression
( "?" Expression ":" ConditionalExpression )?
;
AssignmentExpression ::= ConditionalExpression | Assignment ;
Assignment ::= LeftHandSide AssignmentOperator AssignmentExpression ;
LeftHandSide ::= ExpressionName | FieldAccess | ArrayAccess ;
AssignmentOperator ::= "="
| "*="
| "/="
| "%="
| "+="
| "-="
| "<<="
| ">>="
| ">>>="
| "&="
| "^="
| "|="
;
Expression ::= AssignmentExpression ;
ConstantExpression ::= Expression ;
|
Из за большого объема этот материал размещен на нескольких страницах:
1 2 3 4 |
