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

Синтаксис

SE_SpecificationBlock ::= "specification"

( SE_AccessDescription )*

"{"

SE_PreBlock

( SE_MethodSpecification )+

"}"

;

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

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

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

Ограничения доступа, указанные в группе спецификаций, должны быть повторены без ослабления у каждого спецификационного метода этой группы В предусловии группы спецификаций и до него нельзя вызывать спецификационные методы Перед предусловием группы спецификаций, если оно присутствует, и после него, но до начала объявлений спецификационных методов, нельзя использовать операторы return и throws

Пример

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

// описывающей две операции для работы с очередью:

// первая возвращает первый элемент очереди, вторая – последний

specification

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

// поле items хранит элементы очереди

reads items.? // поля поля items доступны только на чтение

{

// предусловие группы спецификаций

pre

{

// очередь должна быть не пустой

return !items. isEmpty();

}

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

// описывающего операцию, возвращающую первый элемент очереди

specification public Object getFirstElement()

reads items.?

{

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

post

{

// определение единственной ветви функциональности

branch "Single branch";

return getFirstElement == items. firstElement();

}

}

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

// описывающего операцию, возвращающую последний элемент очереди

specification public Object getLastElement()

reads items.?

{

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

post

{

// определение единственной ветви функциональности

branch "Single branch";

return getLastElement == items. lastElement();

}

}

}

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

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

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

На языке *****@***тестовое покрытие описывается в терминах спецификации. В языке определены следующие стандартные тестовые покрытия:

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

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

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

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

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

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

Ветви функциональности помечаются при помощи оператора branch (см. раздел Оператор branch).

Пример

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

// описывающего добавление элемента в очередь

specification public void enq(Object obj)

reads obj, MAX_SIZE // параметр obj и поле MAX_SIZE

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

updates items.? // для полей поля items возможен

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

{

post

{

// если очередь заполнена или obj равен null

if(items. size() == MAX_SIZE || obj == null)

{

branch "No objects added";

// элемент не добавляется

return items. equals(@items. clone());

}

else

{

branch "Object added";

// элемент добавляется в конец очереди

List new_items = (List)(@items. clone());

new_items. addLastElement(obj);

return items. equals(new_items);

}

}

}

Для данного примера покрытие ветвей функциональности выделяет два вида ситуаций:

No objects added – добавление элемента невозможно, так как очередь заполнена или добавляемый элемент равен null Object added – добавление элемента возможно

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

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

Пример

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

// описывающего добавление элемента в очередь

specification public void enq(Object obj)

reads obj, MAX_SIZE // параметр obj и поле MAX_SIZE

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

updates items.? // для полей поля items возможен

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

{

post

{

// если очередь заполнена или obj равен null

if(items. size() == MAX_SIZE || obj == null)

{

branch "No objects added";

// элемент не добавляется

return items. equals(@items. clone());

}

else

{

// выделяем ситуацию, когда очередь пуста

if(items. size() == 0) mark "Empty queue";

branch "Object added";

// элемент добавляется в конец очереди

List new_items = (List)(@items. clone());

new_items. addLastElement(obj);

return items. equals(new_items);

}

}

}

Для данного примера покрытие помеченных путей выделяет три вида ситуаций:

(No objects added) – добавление элемента невозможно, так как очередь заполнена или добавляемый элемент равен null (Empty queue, Object added) – добавление элемента возможно и очередь пуста (Object added) – добавление элемента возможно и очередь не пуста

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

В покрытии предикатов к одному виду относятся ситуации, соответствующие одному и тому же пути по потоку управления в пред- и постусловии одного спецификационного метода (см. раздел Спецификационные методы), оканчивающемуся оператором branch (см. раздел Оператор branch).

Пример

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

// описывающего добавление элемента в очередь

specification public void enq(Object obj)

reads obj, MAX_SIZE // параметр obj и поле MAX_SIZE

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

updates items.? // для полей поля items возможен

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

{

post

{

// если очередь заполнена или obj равен null

if(items. size() == MAX_SIZE || obj == null)

{

branch "No objects added";

// элемент не добавляется

return items. equals(@items. clone());

}

else

{

// выделяем ситуацию, когда очередь пуста

if(items. size() == 0) mark "Empty queue";

branch "Object added";

// элемент добавляется в конец очереди

List new_items = (List)(@items. clone());

new_items. addLastElement(obj);

return items. equals(new_items);

}

}

}

Для данного примера покрытие предикатов выделяет три вида ситуаций:

items.size() == MAX_SIZE || obj == null – добавление элемента невозможно, так как очередь заполнена или добавляемый элемент равен null

!(items.size() == MAX_SIZE || obj == null) && (items.size() == 0) – добавление элемента возможно и очередь пуста !(items.size() == MAX_SIZE || obj == null) && !(items.size() == 0) – добавление элемента возможно и очередь не пуста

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

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

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

Элементарной логической формулой называется логическое выражение, участвующее в одном из ветвлений в пред - или постусловии до оператора branch по потоку управления. Такое выражение должно быть элементарным, то есть не должно быть построено из других логических выражений при помощи операций конъюнкции && или &, дизъюнкции || или |, отрицания !, импликации =>, равенства ==, неравенства != или условного оператора ?:.

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

В силу смысловых связей между элементарными логическими формулами не все комбинации их значений являются достижимыми, что приводит к невозможности достижения 100% покрытия дизъюнктов. Для указания таких связей служит оператор tautology (см. раздел Оператор tautology).

Пример

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

// описывающего добавление элемента в очередь

specification public void enq(Object obj)

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

updates items.? // для полей поля items возможен произвольный доступ

{

post

{

// если очередь заполнена или obj равен null

if(items. size() == MAX_SIZE || obj == null)

{

branch "No objects added";

// элемент не добавляется

return items. equals(@items. clone());

}

else

{

// выделяем ситуацию, когда очередь пуста

if(items. size() == 0) mark "Empty queue";

branch "Object added";

// элемент добавляется в конец очереди

List new_items = (List)(@items. clone());

new_items. addLastElement(obj);

return items. equals(new_items);

}

}

}

Для данного примера покрытие дизъюнктов выделяет четыре вида ситуаций, соответствующие следующим наборам значений элементарных логических формул (items.size() == MAX_SIZE), (obj == null) и (items.size() == 0):

(true, undefined, undefined) – очередь заполнена (false, true, undefined) – добавляемый элемент равен null (false, false, true) – добавление возможно и очередь пуста (false, false, false) – добавление возможно и очередь не пуста

Оператор coverage

Назначение

Оператор coverage предназначен для описания тестового покрытия, отличного от стандартного (см. раздел Описание тестового покрытия).

Описание

Конструкция coverage <идентификатор> = <подпокрытие1>, ... , <подпокрытиеn>; определяет тестовое покрытие с указанным идентификатором, состоящее из подмножеств области определения (возможно пересекающихся), описанных в перечисленных подпокрытиях.

Каждое подпокрытие определяет семейство множеств и может быть представлено следующими способами:

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

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

Идентификатор ранее определенного покрытия или идентификатор стандартного покрытия:

·  branch_coverage – для покрытия ветвей функциональности (см. раздел Покрытие ветвей функциональности)

·  mark_coverage – для покрытия помеченных путей (см. раздел Покрытие помеченных путей)

·  predicate_coverage – для покрытия предикатов (см. раздел Покрытие предикатов)

·  disjunct_coverage – для покрытия дизъюнктов (см. раздел Покрытие дизъюнктов)

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

product(<подпокрытие11>, ... , <подпокрытие1n>; <подпокрытие21>, ... , <подпокрытие2m>) – произведение покрытий

В этом случае, подпокрытие определяет семейство множеств, содержащее все непустые попарные пересечения элементов двух семейств, описанных до и после точки с запятой: первый элемент из первого, второй – из второго

partition(<подпокрытие1>, ... , <подпокрытиеn>) – полное разбиение покрытия

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

complement(<подпокрытие1>, ... , <подпокрытиеn>) – дополнение покрытия

В этом случае, подпокрытие определяет семейство множеств, получаемое добавлением к существующему семейству дополнения объединения его элементов до области определения метода

Оператор coverage должен употребляться в рамках тела спецификационного метода после постусловия (см. раздел Спецификационные методы).

Синтаксис

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 ")"

;

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

Оператор coverage может использоваться только в рамках тела спецификационного метода после постусловия Выражение, используемое для описания подпокрытия, должно иметь тип boolean, либо быть идентификатором уже определенного покрытия, либо быть идентификатором стандартного покрытия – branch_coverage, mark_coverage, predicate_coverage или disjunct_coverage Идентификаторы branch_coverage, mark_coverage, predicate_coverage и disjunct_coverage, а также операторы partition, complement и product могут использоваться только внутри операторов coverage

Пример

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

specification public static long sum(int x, int y)

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

reads x, y // параметры х и y доступны только на чтение

{

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

post

{

// выделяем ситуацию, когда параметр x равен нулю

if(x == 0) mark "x is zero";

// выделяем ситуацию, когда параметр y равен нулю

if(у == 0) mark "y is zero";

// объявление единственной ветви функциональности

branch "Single branch";

return sum == (long)x + (long)y;

}

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

// всевозможные комбинации граничных значений параметров x и y

coverage Coverage1 =

product(x == Integer. MIN_VALUE, x == Integer. MAX_VALUE;

y == Integer. MIN_VALUE, y == Integer. MAX_VALUE);

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

// все четверти системы координат XY, то есть области:

// (x > 0 && y > 0), (x < 0 && y > 0),

// (x < 0 && y < 0), (x > 0 && y < 0)

coverage Coverage2 =

partition(x < 0, x > 0, y < 0, y > 0);

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

// ситуации когда сумма параметров x и y больше максимального

// значения типа int, когда сумма меньше минимального

// значения типа int и когда сумма представима числом типом int

coverage Coverage3 =

complement((long)x + (long)y > Integer. MAX_VALUE,

(long)x + (long)y < Integer. MIN_VALUE);

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

return (long)x + (long)y;

}

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

Назначение

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

Описание

Модификаторы irrelevant могут использоваться только внутри пред- и постусловий спецификационных методов и предусловий групп спецификаций (см. разделы Спецификационные методы и Группы спецификаций соответственно).

Помимо блоков, помеченных модификатором irrelevant, несущественными блоками являются блоки циклов и блоки try, catch и finally.

Внутри несущественных блоков нельзя использовать операторы branch и mark, так как они используются для определения тестового покрытия (см. разделы Оператор branch и Оператор mark соответственно), а также операторы return.

Синтаксис

SE_IrrelevantStatement ::= "irrelevant" Statement ;

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

Модификаторы irrelevant могут использоваться только внутри предусловий групп спецификаций и пред- и постусловий спецификационных методов Внутри несущественных блоков нельзя использовать операторы branch, mark и return

Пример

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

specification public static int max(int x, int y)

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

reads x, y // параметры x и y доступны только на чтение

{

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

post

{

int z = x;

// несущественный блок, содержащий вспомогательные вычисления

irrelevant

{

if(x < y)

z = y;

}

// объявление единственной ветви функциональности

branch "Single branch";

return max == z;

}

}

Оператор tautology

Назначение

Смысловые связи между элементарными логическими формулами (см. раздел Покрытие дизъюнктов) приводят к тому, что не все комбинации их значений являются достижимыми, что искажает тестовое покрытие (см. раздел Описание тестового покрытия). Например, комбинация month(date) == 2 и day(date) == 31, где month – метод, возвращающий номер месяца, а day – день, недостижима.

Оператор tautology предназначен для указания таких смысловых связей между элементарными логическими формулами.

Описание

Оператор tautology имеет единственный параметр, являющийся логическим выражением.

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

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

Синтаксис

SE_Tautology ::= "tautology" Expression ";" ;

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

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

Пример

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

specification package model;

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

public class EmployeeManagementSpecification

{

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

// описывающего операцию, возвращающего зарплату

// сотрудника с начала текущего месяца

specification public double getSalary()

{

post

{

// месяц может изменяться в пределах от 1 до 12

tautology month(date) >= 1 && month(date) <= 12;

// день может изменяться в пределах от 1 до 31

tautology day(date) >= 1 && day(date) <= 31;

// в апреле, июне, сентябре и ноябре 30 дней

tautology (month(date) == 4 || month(date) == 6 ||

month(date) == 9 || month(date) == 11) => day(date) <= 30;

// в феврале не более 29 дней

tautology month(date) == 2 => day(date) <= 29;

// получаем текущее время

long date = System. currentTimeMillis();

switch(month(date))

{

case 1:

mark "January";

break;

case 2:

mark "February";

break;

...

case 12:

mark "December";

break;

}

// ситуация, когда номер месяца меньше 1 или больше 12

// недостижима, эта связь указана в первом операторе tautology

// в последний день длинного месяца дают премию

if(day(date) == 31)

mark "Bonus";

// в феврале, апреле, июне, сентябре и ноябре меньше 31 дня,

// для этих месяцев ситуация, когда день равен 31, недостижима,

// эта связь указана в третьем и четвертом операторах tautology

// определяем единственную ветвь функциональности

branch "Single branch";

...

}

}

// объявление вспомогательных методов

private int year(long date)

{

...

}

private int month(long date)

{

...

}

private int day(long date)

{

...

}

...

}

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

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

Назначение

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

Описание

Наследование спецификационных классов задается обычной конструкцией языка программирования Java extends.

Язык *****@***предоставляет возможность повторного использования пред- и постусловий спецификационного метода (см. разделы Предусловие и Постусловие соответственно). Это достигается с помощью наследования функциональности спецификационного метода в совпадающем по сигнатуре спецификационном методе подкласса. Для этих целей служит конструкция refines super, которая должна располагаться сразу после описания ограничений доспупа (см. раздел Описание ограничений доступа).

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

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

Синтаксис

( "extends" ClassType )?

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

Спецификационные классы могут наследовать только спецификационные классы

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

Если спецификационный метод наследует функциональность, то в базовом классе должен быть объявлен спецификационный метод с такой же сигнатурой

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

·  Если в наследуемом методе указан модификатор доступа reads, то в наследующем методе должен быть указан модификатор доступа reads или updates

·  Если в наследуемом методе указан модификатор доступа writes, то в наследующем методе должен быть указан модификатор доступа writes или updates

·  Если в наследуемом методе указан модификатор доступа updates, то в наследующем методе должен быть тоже указан модификатор доступа updates

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

Пример

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

specification package model;

// импортирование вспомогательного класса, реализующего список

import util. List;

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

// описывающего очередь

public class QueueSpecification

{

// объявление поля items, хранящего элементы очереди

public List items = new List();

// объявление спецификационного метода enq, описывающего

// добавление элемента в конец очереди

specification public void enq(Object obj)

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

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

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

{

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

pre { return obj!= null; }

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

post

{

// выделяем ситуацию когда очередь пуста

if(items. isEmpty()) mark "Empty queue";

// определяем единственную ветвь функциональности

branch "Single branch";

// проверяем, что в конец очереди добавился элемент obj

List new_items = (List)(@items. clone());

new_items. addLastElement(obj);

return items. equals(new_items);

}

}

...

}

Ниже приводится фрагмент объявления спецификационного класса PQueueSpecification, наследующего спецификационный класс QueueSpecification.

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

specification package model;

// импортирование вспомогательного класса, реализующего список

import util. List;

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

// описывающего очередь с приоритетами и наследующего

// спецификационный класс QueueSpecification

public class PQueueSpecification extends QueueSpecification

{

// поле items, хранящее элементы очереди, наследуется от

// спецификационного класса QueueSpecification

// объявление поля priorities, хранящего приоритеты элементов очереди

public List priorities = new List();

// объявление спецификационного метода enq, описывающего

// добавление элемента с минимальным приоритетом в очередь

specification public void enq(Object obj)

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

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

updates items.?, // к полям полей items и priorities

priorities.? // возможен произвольный доступ

refines super // указываем, что спецификационный метод enq

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

// метода базового класса

{

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

pre { return obj != null; }

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

post

{

// выделяем ситуацию когда очередь пуста

if(items. isEmpty()) mark "Empty queue";

// определяем единственную ветвь функциональности

branch "Single branch";

// проверяем, что в конец списка приоритетов добавился

// элемент new Priority(), представляющий минимальный приоритет

List new_priorities = (List)(@priorities. clone());

new_priorities. addLastElement(new Priority());

// проверку списка элементов писать не нужно, так как она

// уже написана в постусловии наследуемого метода

return priorities. equalsByElement(new_priorities);

}

}

...

}

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

Назначение

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

Описание

Уточнение спецификационных классов задается конструкцией refines с дополнительными элементами up и down, после которых указываются имена медиаторных классов (см. раздел Медиаторные классы).

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

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

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

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

Синтаксис

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

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

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

Спецификационные классы могут уточнять только спецификационные классы Для уточнения вида SpecificationClass1 refines SpecificationClass2 up UpMediator down DownMediator должны выполняться следующие условия:

·  Медиаторный класс UpMediator должен быть наследником SpecificationClass1 и иметь ровно одну реализационную ссылку (см. раздел Реализационные ссылки), которая должна иметь тип SpecificationClass2

·  Медиаторный класс DownMediator должен быть наследником SpecificationClass2 и иметь ровно одну реализационную ссылку, которая должна иметь тип SpecificationClass1

·  Спецификационный метод может иметь refines UpMediator, только если содержащий его класс уточняет некоторый спецификационный класс с использованием конструкции refines с дополнительными элементами up и down, причем, после up указан медиаторный класс UpMediator

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

Пример

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