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

// объявление спецификационного класса 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.? // к полям объекта возможен произвольный доступ

{...}

// объявление эквивалентности E

equivalence int E(int item)

// описание ограничений доступа эквивалентности E

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

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

{

// описание первой альтернативы

alternative

{

push(item);

return pop();

}

// описание второй альтернативы

alternative

{

return item;

}

}

...

}

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

Назначение

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

Описание

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

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

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

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

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

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

Синтаксис

SE_MethodSpecification ::= "specification"
SE_MethodHeader
"{"
SE_PreBlock
SE_PostCondition
( BlockStatement )*
"}"
;

SE_MethodHeader ::= MethodHeader

( "refines" SE_Refined ( "," SE_Refined )* )?

;

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 ;

SE_Refined ::= ClassType | "super" ;

Throws ::= "throws" ClassType ( "," ClassType )* ;

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

Грамматику элементов SE_PreCondition, SE_PostCondition и SE_AccessDescription можно найти в разделах Предусловие, Постусловие и Описание ограничений доступа соответственно.

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

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

Пример

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

// операцию добавления элемента в очередь

specification public void enq(Object obj)

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

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

{

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

pre { return obj!= null; }

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

post

{

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

branch "Single branch";

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

new_items. addLastElement(obj);

return items. equals(new_items);

}

}

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

Назначение

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

Описание

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

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

Синтаксис

Throws ::= "throws" ClassType ( "," ClassType )* ;

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

Описываемые классы исключений должны быть производными от класса java.lang.Throwable

Пример

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

specification public Object pop()

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

throws StackIsEmptyException

{

...

}

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

Назначение

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

Описание

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

Язык *****@***поддерживает три вида ограничений доступа:

Только на чтение Только на запись Произвольный доступ

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

Для указания доступа только на чтение используется модификатор reads, только на запись – writes, для указания произвольного доступа – updates. Действие модификатора доступа распространяется на все перечисленные вслед за ним через запятую идентификаторы до следующего модификатора, ключевого слова refines или открывающейся фигурной скобки.

Для сокращения записи можно использовать расширенные идентификаторы, то есть специальные выражения: obj.? или obj.*. Первое означает все поля объекта obj, второе – все объекты, достижимые по ссылкам из объекта obj. В описании ограничений доступа также можно указывать элементы массивов.

Будем говорить, что на идентификатор identifier указан доступ, если либо доступ указан непосредственно на идентификатор identifier, либо – на obj.?, и identifier есть obj.field, где field неквалифицированный идентификатор, либо – на obj.* и identifier есть obj.reference, где reference произвольный идентификатор, либо identifier есть this.reference и доступ указан на reference.

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

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

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

Синтаксис

SE_AccessDescription ::= SE_AccessModifier

SE_Access ( “,” SE_Access )*

;

SE_AccessModifier ::= “reads” | “writes” | “updates” ;

SE_Access ::= ( ( Primary

| ExpressionName

| ( ClassName “.” )? “super”

) “.”

)?

( Identifier | “?” | “*” )

| ArrayAccess

;

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

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

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

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

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

То же справедливо спецификационного метода, наследующего функциональность (см. раздел Наследование спецификационных классов)

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

Пример

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

specification package model;

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

public class AccountSpecification

{

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

static public int maximumCredit;

public int balance;

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

specification public void deposit(int sum)

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

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

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

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

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

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

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

{...}

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

specification public int withdraw(int sum)

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

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

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

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

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

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

{...}

}

Предусловие

Назначение

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

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

Описание

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

Этот набор инструкций заключается в фигурные скобки и помечается ключевым словом pre.

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

Синтаксис

SE_PreCondition ::= "pre" Block ;

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

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

Пример

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

specification public static double log(double x)

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

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

{

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

pre { return x > 0; }

...

}

Постусловие

Назначение

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

Во время тестирования постусловие проверяется всякий раз после вызова операции целевой системы, и, если оно нарушено, значит при данном обращении к операции ее поведение не соответствовало спецификации (см. раздел Спецификации).

Описание

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

Этот набор инструкций заключается в фигурные скобки и помечается ключевым словом post.

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

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

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

Синтаксис

SE_PostCondition ::= "post" Block ;

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

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

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

·  Идентификатор спецификационного метода для обозначения результата его вызова, в случае если тип результата отличен от void и thrown == null

·  Ключевое слово thrown для обозначения возникшего исключения

В постусловиях нельзя использовать несущественные блоки, содержащие операторы return (см. раздел Модификатор irrelevant).

Пример

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

specification public static double log(double x)

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

throws IllegalArgumentException

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

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

{

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

post

{

if(x <= 0)

{

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

// для случая, когда аргумент не входит в

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

branch "Exceptional case";

return thrown != null &&

thrown instanceof IllegalArgumentException;

}

else

{

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

// для случая, когда аргумент входит в

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

branch "Normal execution";

return thrown == null &&

(Math. power(Math. E, log) - x) / x < 1.e - 12;

}

}

}

Оператор branch

Назначение

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

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

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

Описание

Оператор branch имеет единственный параметр – строковый литерал, служащий для именования ветви функциональности.

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

Каждое вхождение оператора branch трактуется как место обращения к операции целевой системы. Все инструкции, написанные до оператора branch по потоку управления, выполняются до обращения к операции, после оператора branch – после ее выполнения.

Исключения составляют превыражения (см. раздел Превыражения), помечаемые префиксным оператором @: они должны располагаться после оператора branch по потоку управления, но вычисляются до выполнения операции целевой системы.

Синтаксис

SE_BranchStatement ::= "branch" <StringLiteral> ";" ;

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

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

Операторы branch нельзя использовать внутри несущественных блоков (см. раздел Модификатор irrelevant)

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

Пример

// объявление спецификационного метода 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;

}

}

}

Оператор mark

Назначение

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

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

Описание

Оператор mark имеет единственный параметр – строковый литерал, именующий пометку пути.

Синтаксис

SE_MarkStatement ::= "mark" <StringLiteral> ";" ;

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

Операторы mark можно использовать только в предусловии групп спецификаций, пред - или постусловиях спецификационных методов

Операторы mark нельзя использовать внутри несущественных блоков (см. раздел Модификатор irrelevant)

Пример

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

specification public int withdraw(int sum)

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

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

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

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

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

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

{

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

pre { return sum > 0; }

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

post

{

// помечаем пути в зависимости от значения поля balance

if(balance > 0)

mark "Withdrawal from account with positive balance";

else if(balance == 0)

mark "Withdrawal from empty account";

else

mark "Withdrawal from account with negative balance";

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;

}

}

}

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

Назначение

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

Значение выражения до выполнения операции целевой системы называется его пре-значением, после – пост-значением.

Описание

Превыражения помечаются при помощи префиксного оператора @ и должны располагаться после оператора branch по потоку управления.

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

Приоритет оператора @ меньше приоритета оператора . , но больше приоритета операторов *, / и % Вычислимость превыражения должна быть обеспечена непосредственно перед оператором branch, находящимся до него по потоку управления, в частности, внутри превыражения можно использовать идентификаторы только тех локальных переменных, которые объявлены до оператора branch по потоку управления

Синтаксис

"@" UnaryExpression ;

UnaryExpression ::= PreIncrementExpression

| PreDecrementExpression

| "+" UnaryExpression

| "-" UnaryExpression

| UnaryExpressionNotPlusMinus

;

PreIncrementExpression ::= "++" UnaryExpression ;

PreDecrementExpression ::= "--" UnaryExpression ;

UnaryExpressionNotPlusMinus ::= PostfixExpression

| "~" UnaryExpression

| "!" UnaryExpression

| CastExpression

| "@" UnaryExpression

;

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

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

В спецификации конструктора нельзя использовать презначения полей объекта класса, конструктор которого специфицируется

Пример

// объявление спецификационного метода 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";

// баланс счета после вызова метода (balance) равен

// балансу счета до вызова метода (@balance),

// увеличенному на сумму вклада (sum)

return balance == @balance + sum;

}

}

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

Назначение

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

Описание

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

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

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