версия 2.3
// development storage for h1 level headers
Данный документ представляет собой справочник по языку JavaTESK. В нем содержится описание конструкций языка, их синтаксис, связанные с ними семантические ограничения и примеры их использования для разработки тестов.
Документ предназначен пользователям инструмента JavaTESK и входит в комплект документации, поставляемой с ним.
Документ состоит из следующих разделов:
В документе используются следующие шрифтовые и цветовые выделения:
// объявление пакета model package model; // объявление спецификационного класса SpecificationClass public class SpecificationClass { ... }
Дополнительную информацию по инструменту JavaTESK и технологии тестирования UniTESK можно найти в следующих источниках:
Процесс тестирования должен демонстрировать, что целевая система (то есть система, для которой разрабатываются тесты) удовлетворяет требованиям, предъявляемым к ней, на некотором достаточно показательном наборе ситуаций. Для этой цели при разработке тестов необходимо иметь полное и точное описание требований к целевой системе. Дополнительно нужно определить набор тестовых ситуаций, на котором будет проводиться тестирование.
Технология тестирования UniTESK сфокусирована на функциональном тестировании, нацеленным на проверку соответствия целевой системы функциональным требованиям (то есть, требованиям, описывающим, что система должна делать). Одна из основных целей UniTESK – автоматизировать насколько это возможно процесс функционального тестирования.
Функциональные требования пишутся в форме спецификаций, которые состоят из описания интерфейса целевой системы, описания ограничений на значения ее данных и описания корректного поведения ее операций.
Спецификации, представляемые в формальной, понятной компьютеру форме, называются формальными спецификациями. Из формальных спецификаций можно автоматически генерировать оракулы, проверяющие соответствие поведения целевой системы требованиям, записанным в спецификациях.
Привязку спецификаций к целевой системе осуществляют специальные компоненты тестовой системы, называемые медиаторами.
Как описать достаточный набор тестовых ситуаций?
Обычный способ сделать это – определить некоторую метрику тестового покрытия и значение этой метрики, достаточное для того, чтобы считать, что целевая система качественно протестирована. Примеры широко используемых на практике метрик: процент исполненных во время тестирования операций и процент строк исходного кода, покрываемых тестом.
При функциональном тестировании высокий уровень покрытия строк исходного кода еще недостаточен, чтобы утверждать, что целевая система качественно протестирована, хотя и важен для демонстрации того, какие части реализации протестированы.
Поэтому рассматриваются метрики тестового покрытия заданные в терминах функциональности целевой системы, а не в терминах исходного кода. Поскольку спецификации формально представляют функциональные требования, метрики, определенные в терминах структуры спецификации (например, процент ветвей функциональности, покрываемых тестом), гораздо лучше соответствуют функциональности, чем метрики, основанные на исходном коде.
Когда есть описание функциональности целевой системы и значение метрики тестового покрытия, которое нужно достичь, остается единственная проблема – генерация тестовой последовательности(то есть последовательности обращений к операциям целевой системы) для достижения заданного тестового покрытия.
Описание тестовой последовательности называется тестовым сценарием.
Технология тестирования UniTESK предлагает специальную технику для описания тестовых сценариев, основанную на понятии конечных автоматов. Язык JavaTESK позволяет описывать автоматную модель целевой системы в компактной, удобной для повторного использования форме. По данному описанию автоматически строится обход графа состояний конечного автомата, в результате которого генерируется требуемая тестовая последовательность.
Язык JavaTESK является расширением языка программирования Java и специально разработан для поддержки технологии тестирования UniTESK.
В нем есть специальные конструкции, которые позволяют компактным и удобным образом описывать функциональные требования к целевой системе и тестовые последовательности.
Это делает разработку тестов максимально удобной, а также позволяет сократить затраты на обучение разработчиков тестов, уже знакомых с языком программирования Java.
В язык JavaTESK введены четыре специальных вида классов:
Их объявления должны находится в файлах с расширением sej.
Для всех видов специальных классов должны выполняться следующие общие семантические ограничения.
Виды специальных методов:
К некоторым видам специальных методов относятся не все изложенные в данном разделе требования. Например, инварианты не имеют параметров, поэтому требование 3 для них не имеет смысла. Отоносится ли некоторое общее требование к данному конкретному виду специальных методов, определяется наличием синтаксических конструкций, используемых в требовании, в синтаксическом определении декларации методов данного вида.
В язык JavaTESK введены два дополнительных оператора:
Оператор импликации введен для удобства чтения и записи логических выражений. Он является бинарным инфиксным оператором, приоритет которого меньше приоритета оператора дизъюнкции ||, но больше приоритета условного оператора ?:.
Выражение x => y эквивалентно выражению !x || y, и при его вычислении, также как при вычислении других логических операторов, действуют правила короткой логики.
Оператор импликации ассоциативен справа налево, то есть выражение x => y => z эквивалентно выражению x => (y => z).
В язык JavaTESK введены дополнительные ключевые слова, которые нельзя использовать в качестве идентификаторов:
Спецификации представляют собой формальное описание функциональных требований к целевой системе в форме инвариантов данных и спецификационных методов (см. разделы Инварианты данных и Спецификационные методы соответственно).
Следуя концепии объектно-ориентированного программирования, реализованной в языке программирования Java, спецификации на языке JavaTESK пишутся в виде набора спецификационных классов (см. раздел Спецификационные классы).
Для описания требований спецификации могут использовать как непосредственно данные целевой системы, так и собственную спецификационную модель данных, то есть совокупность структур данных, хранящих информацию об истории взаимодействия целевой системы с окружением и используемых для спецификации ее поведения.
Привязка данных спецификационной модели к данным целевой системы и спецификационных методов к операциям целевой системы осуществляется при помощи медиаторов (см. раздел Медиаторы).
Спецификационные классы являются основными структурными единицами спецификации.
Обычно каждый спецификационный класс содержит описание требований к некоторому компоненту целевой системы.
Спецификационные классы оформляются как обычные классы Java и могут содержать следующие объявления:
Язык JavaTESK поддерживает наследование и уточнение спецификационных классов (см. разделы Наследование спецификационных классов и Уточнение спецификационных классов соответственно).
SE_SpecificationClassDeclaration ::= SE_ClassModifiers "specification" UnmodifiedClassHeader ( SE_ClassRefinement ( "," SE_ClassRefinement )* )? SE_SpecificationClassBody ; SE_ClassModifiers ::= ( "abstract" | "strictfp" | "final" | Annotation )* ; UnmodifiedClassHeader ::= "class" Identifier ( TypeParameters )? ( Super )? ( Interfaces )? ; SE_SpecificationClassBody ::= "{" ( SE_SpecificationClassBodyDeclaration )* "}" ; SE_SpecificationClassBodyDeclaration ::= ClassBodyDeclaration | SE_InvariantDeclaration | SE_OperationSpecification ; SE_OperationSpecification ::= SE_MethodSpecification | SE_ReactionSpecification ;
Грамматику элементов SE_InvariantDeclaration и SE_MethodSpecification можно найти в разделах Инварианты данных и Спецификационные методы соответственно.
// объявление спецификационного класса AccountSpecification specification class AccountSpecification { // объявление полей спецификационной модели данных static public int maximumCredit; public int balance; // объявление конструктора спецификационного // класса AccountSpecification public AccountSpecification() { } // объявление инварианта данных I invariant I() { return balance >= -maximumCredit; } // объявление спецификационного метода deposit specification void deposit(int sum) { // предусловие спецификационного метода deposit pre { return (0 < sum ) && (balance <= Integer.MAX_VALUE - sum); } // постусловие спецификационного метода deposit post { branch Single; return balance == pre balance + sum; } } // объявление спецификационного метода withdraw specification int withdraw(int sum) { // предусловие спецификационного метода withdraw pre { return sum > 0; } // постусловие спецификационного метода withdraw post { if(balance < sum - maximumCredit) { branch TooLargeSum("Withdrawn sum is too large"); return balance == pre balance && withdraw == 0; } else { branch Normal("Successful withdrawal"); return balance == pre balance - sum && withdraw == sum; } } } }
Инварианты данных предназначены для описания ограничений на значения полей спецификационной модели данных (см. раздел Спецификации).
С одной стороны, их можно рассматривать как ограничения подтипа, определяющие целостность спецификационной модели данных, с другой – как общие части пред- и постусловий всех спецификационных методов (см. раздел Спецификационные методы) спецификационного класса (см. раздел Спецификационные классы).
Инварианты данных могут объявляться только в спецификационных классах и представляются как методы без параметров, помеченные модификатором invariant и возвращающие значение типа boolean: true – если данные удовлетворяют ограничениям, false – иначе. Поскольку тип возвращаемого значения фиксирован, он не указывается.
Спецификационный класс может содержать несколько объявлений инвариантов данных, при этом проверяется конъюнкция задаваемых ими ограничений.
Инварианты данных могут быть статическими. Такие инварианты помечаются модификатором static и могут описывать ограничения только на статические поля спецификационной модели данных.
SE_InvariantDeclaration ::= ( SE_CommonModifier | "prime" )* "invariant" Identifier "(" ( <STRING_LITERAL> )? ")" Block ; SE_CommonModifier ::= "static" | "strictfp" | Annotation ;
Определение: в блоке Block существует необработанный ThrowStatement, если
При проверках, связанных с перегрузкой методов при наследовании, инварианты рассматриваются аналогично обычным Java-методам с типом возвращаемого значения boolean и пустым списком параметров.
// объявление спецификационного класса TimeSpecification specification class TimeSpecification { // объявление полей спецификационной модели данных int hour; int minute; // объявление инварианта, описывающего ограничения // на значения поля hour invariant hours() { // часы могут изменяться в пределах от 0 до 23 return hour >= 0 && hour <= 23; } // объявление инварианта, описывающего ограничения // на значения поля minute invariant minutes() { // минуты могут изменяться в пределах от 0 до 59 return minute >= 0 && minute <= 59; } ... }
Спецификационные методы предназначены для описания поведения операций целевой cистемы в форме пред- и постусловий (см. разделы Предусловие и Постусловие соответственно).
Спецификационные методы объявляются в спецификационных классах (см. раздел Спецификационные классы) и помечаются модификатором specification, который должен располагаться после всех других модификаторов.
Спецификационные методы могут перегружать спецификационные методы, а также наследовать и уточнять их функциональность (см. раздел Связи между спецификациями).
Спецификационные методы могут быть перегружены медиаторными методами медиаторных классов (см. раздел Медиаторные классы).
Объявление спецификационного метода включает:
Под телом спецификационного метода понимается набор инструкций, заданных в нем, за исключением тех, которые образуют пред- и постусловие. Инструкции, расположенные в спецификационном методе перед предусловием, являются общей частью тела метода, пред- и постусловия, инструкции, расположенные в спецификационном методе между пред- и постусловием, – общей частью тела метода и постусловия.
SE_MethodSpecification ::= ( SE_CommonModifier | "synchronized" )* "specification" SE_MethodHeader SE_MethodBody ; SE_MethodHeader ::= MethodHeader ( SE_OperationRefinement ( "," SE_OperationRefinement )* )? ; MethodHeader ::= ( TypeParameters )? ResultType MethodDeclarator ( Throws )? ;
Грамматику элементов SE_PreCondition и SE_PostCondition можно найти в разделах Предусловие и Постусловие соответственно.
// объявление спецификационного метода enq, описывающего // операцию добавления элемента в очередь specification void enq(Object obj) { // предусловие спецификационного метода enq pre { return obj != null; } // постусловие спецификационного метода enq post { // определяем единственную ветвь функциональности branch Single; List new_items = (List)(pre items.clone()); new_items.addLastElement(obj); return items.equals(new_items); } }
Описание возможных исключений предназначено для указания классов исключений, возникновение которых возможно при нормальной работе операции целевой системы.
Описание возможных исключений следует сразу после сигнатуры спецификационного метода и начинается с ключевого слова throws, после которого через запятую указываются все классы исключений, возникновение которых возможно при нормальной работе операции целевой системы, кроме обрабатываемых самим методом и тех, возникновение которых невозможно при выполнении предусловия (см. раздел Предусловие).
Если небходимо показать, что никаких исключений во время работы метода быть не должно, ничего не пишется.
Throws ::= "throws" ExceptionTypeList ; ExceptionTypeList ::= ExceptionType ( "," ExceptionType )* ; ExceptionType ::= ClassType | TypeVariable ;
// объявление спецификационного метода pop specification Object pop() // описание возможных исключений throws StackIsEmptyException { ... }
Определение: первый список BlockStatement называется блоком инициализаций.
Определение: второй список BlockStatement называется реализационным телом.
SE_MethodBody ::= "{" ( BlockStatement )* ( SE_PreCondition )? ( SE_PostCondition )? ( BlockStatement )* "}" ;
Предусловие служит для выделения ситуаций, в которых определено поведение операции целевой системы, описываемой в спецификационном методе (см. раздел Спецификационные методы).
Во время тестирования предусловие проверяется всякий раз, когда надо вызвать операцию, и если оно нарушено, обращения к целевой системе не происходит.
Предусловие оформляется как набор инструкций, представляющий собой тело метода, имеющего те же параметры, что и спецификационный метод и возвращающего результат типа boolean: true – если при данных значениях параметров поведение операции целевой системы определено, false – иначе.
Этот набор инструкций заключается в фигурные скобки и помечается ключевым словом pre.
Предусловие может быть опущено. Отсутствие предусловия эквивалентно наличию предусловия, всегда возвращающего true.
SE_PreCondition ::= "pre" Block ;
Определеие: будем говорить что некоторая конструкция языка находится в существенном контексте, если она не находится внутри:
Предусловие должно удовлетворять следующим ограничениям:
// объявление статического спецификационного метода log static specification double log(double x) { // предусловие спецификационного метода log pre { return x > 0; } ... }
Постусловие служит для описания ограничений, которым должны удовлетворять результаты работы операции целевой системы, описываемой спецификационным методом (см. раздел Спецификационные методы).
Во время тестирования постусловие проверяется всякий раз после вызова операции целевой системы, и, если оно нарушено, значит при данном обращении к операции ее поведение не соответствовало спецификации (см. раздел Спецификации).
Постусловие оформляется как набор инструкций, представляющий собой тело метода, имеющего те же параметры, что и спецификационный метод и возвращающего результат типа boolean: true – если поведение операции целевой системы соответствует спецификации, false – иначе.
Этот набор инструкций заключается в фигурные скобки и помечается ключевым словом post.
В постусловии должны быть определены ветви функциональности при помощи операторов branch (см. раздел Оператор branch).
Для описания условий возникновения и свойств возникающих исключений используется ключевое слово thrown, которое служит для обозначения исключения, возникшего во время выполнения операции целевой системы. Если во время обращения к операции целевой системы исключения не возникли, то thrown == null
SE_PostCondition ::= "post" Block ;
// объявление статического спецификационного метода log static specification double log(double x) // описание возможных исключений throws IllegalArgumentException { // постусловие спецификационного метода log post { if(x <= 0) { // определение ветви функциональности // для случая, когда аргумент не входит в // область определения спецификационного метода branch Exceptional; return thrown != null && thrown instanceof IllegalArgumentException; } else { // определение ветви функциональности // для случая, когда аргумент входит в // область определения спецификационного метода branch Normal; return thrown == null && (Math.power(Math.E, log) - x) / x < 1.e-12; } } }
Оператор branch предназначен для задания ветвей функциональности в постусловиях спецификационных методов (см. раздел Постусловие).
Под ветвью функциональности понимается подмножество области определения спецификационного метода, на котором поведение соответствующей операции целевой системы описывается одними и теми же выражениями.
Оператор branch используются для разбиения всех тестовых ситуаций в покрытии ветвей функциональности (см. раздел Покрытие ветвей функциональности).
Оператор branch имеет два параметра – идентификатор, служащий для именования ветви функциональности, и строковый литерал - для указания дополнительного комментария.
Идентификаторы, используемые в операторах branch, должны быть уникальными в пределах постусловия спецификационного метода.
Каждое вхождение оператора branch трактуется как место обращения к операции целевой системы. Все инструкции, написанные до оператора branch по потоку управления, выполняются до обращения к операции, после оператора branch – после ее выполнения.
Исключения составляют превыражения (см. раздел Превыражения), помечаемые префиксным оператором pre: они должны располагаться после оператора branch по потоку управления, но вычисляются до выполнения операции целевой системы.
Если оператор branch содержит оператор update, то обновлённое состояния модели, построенное этим оператором update, будет проверяться инвариантами.
SE_BranchStatement ::= "branch" Identifier ( "(" Expression ")" )? ( ";" | SE_UpdateStatement ) ;
// объявление спецификационного метода withdraw specification int withdraw(int sum) { // предусловие спецификационного метода withdraw pre { return sum > 0; } // постусловие спецификационного метода withdraw post { if(balance < sum - maximumCredit) { // определение ветви функциональности // для случая, когда снимаемая сумма слишком большая, // то есть при ее снятии происходит превышение // максимального допустимого размера кредита branch TooLargeSum("Withdrawn sum is too large"); return balance == pre balance && withdraw == 0; } else { // определение ветви функциональности // для случая, когда при снятии указанной суммы // не происходит превышение максимального // допустимого размера кредита branch Normal("Successful withdrawal"); return balance == pre balance - sum && withdraw == sum; } } }
Оператор mark предназначен для пометки путей в пред- и постусловиях спецификационных методов. Он используются для разбиения всех тестовых ситуаций в покрытии помеченных путей (см. раздел Покрытие помеченных путей).
Оператор mark имеет единственный параметр – строковый литерал, именующий пометку пути.
SE_MarkStatement ::= "mark" ( Identifier )? <STRING_LITERAL> ;
// объявление спецификационного метода withdraw specification int withdraw(int sum) { // предусловие спецификационного метода 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 TooLargeSum("Withdrawn sum is too large"); return balance == pre balance && withdraw == 0; } else { // определение ветви функциональности // для случая, когда при снятии указанной суммы // не происходит превышение максимального // допустимого размера кредита branch Normal("Successful withdrawal"); return balance == pre balance - sum && withdraw == sum; } } }
Превыражения предназначены для обозначения выражений, которые расположены в постусловии спецификационного метода (см. раздел Постусловие) после оператора branch (см. раздел Оператор branch) по потоку управления, но вычисляются до выполнения операции целевой системы.
Значение выражения до выполнения операции целевой системы называется его пре-значением, после – пост-значением.
Превыражения помечаются при помощи префиксного оператора pre и должны располагаться после оператора branch по потоку управления.
При записи превыражений следует руководствоваться следующими правилами:
SE_PreExpression ::= "pre" UnaryExpression ; UnaryExpression ::= PreIncrementExpression | PreDecrementExpression | UnaryPlusExpression | UnaryMinusExpression | UnaryExpressionNotPlusMinus ; PreIncrementExpression ::= "++" UnaryExpression ; PreDecrementExpression ::= "--" UnaryExpression ; UnaryPlusExpression ::= "+" UnaryExpression ; UnaryMinusExpression ::= "-" UnaryExpression ; UnaryExpressionNotPlusMinus ::= PostfixExpression | BitwiseComplementExpression | LogicalComplementExpression | CastExpression | SE_PreExpression ;
Определение: тип языка Java является синтаксически выразимым, если он не является wildcard-ом или массивом wildcard-ов.
// объявление спецификационного метода deposit specification void deposit(int sum) { // предусловие спецификационного метода deposit pre { return (0 < sum ) && (balance <= Integer.MAX_VALUE - sum); } // постусловие спецификационного метода deposit post { // баланс счета после вызова метода (balance) равен // балансу счета до вызова метода (pre balance), // увеличенному на сумму вклада (sum) return balance == ( pre balance ) + sum; } }
Тестовое покрытие представляет собой конечный набор видов ситуаций, покрывающий все ситуации, которые могут возникнуть во время тестирования.
Достигнутый во время тестирования уровень покрытия при этом измеряется как отношение количества видов ситуаций, реализовавшихся во время тестирования, к их общему числу.
На языке JavaTESK тестовое покрытие описывается в терминах спецификации. В языке определены следующие стандартные тестовые покрытия:
В покрытии ветвей функциональности к одному виду относятся ситуации, соответствующие одной ветви функциональности в постусловии одного спецификационного метода (см. раздел Постусловие).
Ветви функциональности помечаются при помощи оператора branch (см. раздел Оператор branch).
// объявление спецификационного метода enq, // описывающего добавление элемента в очередь specification void enq(Object obj) { post { // если очередь заполнена или obj равен null if(items.size() == MAX_SIZE || obj == null) { branch NoObjectAdded; // элемент не добавляется return items.equals(pre items.clone()); } else { branch ObjectAdded; // элемент добавляется в конец очереди List new_items = (List)(pre items.clone()); new_items.addLastElement(obj); return items.equals(new_items); } } }
Для данного примера покрытие ветвей функциональности выделяет два вида ситуаций:
В покрытии помеченных путей к одному виду относятся ситуации, соответствующие одной и той же последовательности операторов mark и branch (см. разделы Оператор mark и Оператор branch соответственно), оканчивающейся оператором branch, в пред- и постусловии одного спецификационного метода (см. раздел Спецификационные методы).
// объявление спецификационного метода enq, // описывающего добавление элемента в очередь specification void enq(Object obj) { post { // если очередь заполнена или obj равен null if(items.size() == MAX_SIZE || obj == null) { branch NoObjectsAdded; // элемент не добавляется return items.equals(pre items.clone()); } else { // выделяем ситуацию, когда очередь пуста if(items.size() == 0) mark "Empty queue"; branch ObjectAdded; // элемент добавляется в конец очереди List new_items = (List)(pre items.clone()); new_items.addLastElement(obj); return items.equals(new_items); } } }
Для данного примера покрытие помеченных путей выделяет три вида ситуаций:
В покрытии предикатов к одному виду относятся ситуации, соответствующие одному и тому же пути по потоку управления в пред- и постусловии одного спецификационного метода (см. раздел Спецификационные методы), оканчивающемуся оператором branch (см. раздел Оператор branch).
// объявление спецификационного метода enq, // описывающего добавление элемента в очередь specification void enq(Object obj) { post { // если очередь заполнена или obj равен null if(items.size() == MAX_SIZE || obj == null) { branch NoObjectsAdded; // элемент не добавляется return items.equals(pre items.clone()); } else { // выделяем ситуацию, когда очередь пуста if(items.size() == 0) mark "Empty queue"; branch ObjectAdded; // элемент добавляется в конец очереди List new_items = (List)(pre items.clone()); new_items.addLastElement(obj); return items.equals(new_items); } } }
Для данного примера покрытие предикатов выделяет три вида ситуаций:
В покрытии дизъюнктов к одному виду относятся ситуации, соответствующие одному и тому же набору значений элементарных логических формул (такой набор называется дизьюнктом), определяющих путь по потоку управления в пред- и постусловии одного спецификационного метода (см. разделы Предусловие и Постусловие соответственно), оканчивающегося одним из операторов branch (см. раздел Оператор branch).
Значения некоторых элементарных формул, относящихся к одной ситуации, могут быть неопределены, так как при вычислении логических выражений используется короткая логика, и путь по потоку управления может быть определен на основании значений только некоторых из них.
Элементарной логической формулой называется логическое выражение, участвующее
Такое выражение должно быть элементарным, то есть не должно быть построено из других логических выражений при помощи операций конъюнкции && или &, дизъюнкции || или |, отрицания !, импликации =>, равенства ==, неравенства != или условного оператора ?:.
Элементарные логические формулы отождествляются по текстуальному совпадению, поэтому в условиях ветвлений не должны использоваться разные сущности (параметры спецификационного метода, поля спецификационной модели данных (см. раздел Спецификации) или локальные переменные), имеющие одинаковый идентификатор – это может привести к искажению тестового покрытия.
В силу смысловых связей между элементарными логическими формулами не все комбинации их значений являются достижимыми, что приводит к невозможности достижения 100% покрытия дизъюнктов. Для указания таких связей служит оператор tautology (см. раздел Оператор tautology).
// объявление спецификационного метода enq, // описывающего добавление элемента в очередь specification void enq(Object obj) { post { // если очередь заполнена или obj равен null if(items.size() == MAX_SIZE || obj == null) { branch NoObjectsAdded; // элемент не добавляется return items.equals(pre items.clone()); } else { // выделяем ситуацию, когда очередь пуста if(items.size() == 0) mark "Empty queue"; branch ObjectAdded; // элемент добавляется в конец очереди List new_items = (List)(pre items.clone()); new_items.addLastElement(obj); return items.equals(new_items); } } }
Для данного примера покрытие дизъюнктов выделяет четыре вида ситуаций, соответствующие следующим наборам значений элементарных логических формул (items.size() == MAX_SIZE), (obj == null) и (items.size() == 0):
Модификатор irrelevant предназначен для указания на то, что помеченная им инструкция или блок являются несущественными, то есть содержат вспомогательные вычисления, не учитывающиеся при построения тестового покрытия (см. раздел Описание тестового покрытия).
Модификатор irrelevant может использоваться только внутри пред- и постусловий спецификационных методов (см. разделы Спецификационные методы ).
Помимо блоков, помеченных модификатором irrelevant, несущественными блоками являются блоки циклов и блоки try, catch и finally.
Внутри несущественных блоков нельзя использовать операторы branch и mark, так как они используются для определения тестового покрытия (см. разделы Оператор branch и Оператор mark соответственно), а также операторы return.
SE_IrrelevantStatement ::= "irrelevant" Statement ;
// объявление статического спецификационного метода max specification static int max(int x, int y) { // объявление постусловия спецификационного метода max post { int z = x; // несущественный блок, содержащий вспомогательные вычисления irrelevant { if(x < y) z = y; } return max == z; } }
Смысловые связи между элементарными логическими формулами (см. раздел Покрытие дизъюнктов) приводят к тому, что не все комбинации их значений являются достижимыми, что искажает тестовое покрытие (см. раздел Описание тестового покрытия). Например, комбинация month(date) == 2 и day(date) == 31, где month – метод, возвращающий номер месяца, а day – день, недостижима.
Оператор tautology предназначен для указания таких смысловых связей между элементарными логическими формулами.
Оператор tautology имеет единственный параметр, являющийся логическим выражением.
Он утверждает, что указанное выражение всегда принимает значение true в силу смысловых связей между участвующими в нем элементарными логическими формулами.
SE_TautologyStatement ::= "tautology" Expression ";" ;
// объявление спецификационного класса EmployeeManagementSpecification specification class EmployeeManagementSpecification { // объявление спецификационного метода getSalary, // описывающего операцию, возвращающего зарплату // сотрудника с начала текущего месяца specification 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 ... } } // объявление вспомогательных методов private int year(long date) { ... } private int month(long date) { ... } private int day(long date) { ... } ... }
Наследование спецификационных классов предназначено для обеспечения повторного использования инвариантов данных, аксиом, эквивалентностей и спецификационных методов, описанных в базовом спецификационном классе, в его подклассе (см. разделы Инварианты данных и Спецификационные методы соответственно).
Наследование спецификационных классов задается обычной конструкцией языка программирования Java extends.
Super ::= "extends" ClassType ;
Язык JavaTESK предоставляет возможность повторного использования пред- и постусловий спецификационного метода (см. разделы Предусловие и Постусловие соответственно). Это достигается с помощью наследования функциональности спецификационного метода в совпадающем по сигнатуре спецификационном методе подкласса. Для этих целей служит конструкция refines super, которая должна располагаться в самом конце заголовка декларации спецификационного метода (см. раздел Спецификационные_методы).
Предусловие наследующего функциональность спецификационного метода есть дизъюнкция написанного предусловия и предусловия наследуемого метода, а постусловие – конъюнкция постусловия наследуемого метода и написанного постусловия. Пред- и постусловия вычисляются с учетом короткой логики.
SE_OperationRefinement ::= SE_SuperOperationRefinement | SE_GeneralOperationRefinement ; SE_SuperOperationRefinement ::= "refines" "super" ; SE_GeneralOperationRefinement ::= "refines" ( ClassOrInterfaceType ( "up" Block )? | "up" Block ) ( "down" Block )? ( "update" Block )? ;
// импортирование вспомогательного класса, реализующего список import util.List; // объявление спецификационного класса QueueSpecification, // описывающего очередь specification class QueueSpecification { // объявление поля items, хранящего элементы очереди public List items = new List(); // объявление спецификационного метода enq, описывающего // добавление элемента в конец очереди specification void enq(Object obj) { // предусловие спецификационного метода enq pre { return obj != null; } // постусловие спецификационного метода enq post { // выделяем ситуацию когда очередь пуста if(items.isEmpty()) mark "Empty queue"; // определяем единственную ветвь функциональности branch "Single branch"; // проверяем, что в конец очереди добавился элемент obj List new_items = (List)(pre items.clone()); new_items.addLastElement(obj); return items.equals(new_items); } } ... }
Ниже приводится фрагмент объявления спецификационного класса PQueueSpecification, наследующего спецификационный класс QueueSpecification.
// импортирование вспомогательного класса, реализующего список import util.List; // объявление спецификационного класса PQueueSpecification, // описывающего очередь с приоритетами и наследующего // спецификационный класс QueueSpecification specification class PQueueSpecification extends QueueSpecification { // поле items, хранящее элементы очереди, наследуется от // спецификационного класса QueueSpecification // объявление поля priorities, хранящего приоритеты элементов очереди public List priorities = new List(); // объявление спецификационного метода enq, описывающего // добавление элемента с минимальным приоритетом в очередь specification void enq(Object obj) refines super // указываем, что спецификационный метод enq наследует функциональность // спецификационного метода базового класса { // предусловие спецификационного метода enq pre { return obj != null; } // постусловие спецификационного метода enq post { // выделяем ситуацию когда очередь пуста if(items.isEmpty()) mark "Empty queue"; // проверяем, что в конец списка приоритетов добавился // элемент new Priority(), представляющий минимальный приоритет List new_priorities = (List)(pre priorities.clone()); new_priorities.addLastElement(new Priority()); // проверку списка элементов писать не нужно, так как она // уже написана в постусловии наследуемого метода return priorities.equalsByElement(new_priorities); } } ... }
// currently unsupported
Уточнение спецификационных классов предназначено для обеспечения повторного использования элементов спецификационного класса в спецификационном классе с отличающимся интерфейсом.
Уточнение спецификационных классов задается конструкцией refines с дополнительными элементами up и down, после которых указываются имена медиаторных классов (см. раздел Медиаторные классы).
Медиаторный класс, указанный после ключевого слова up, называется обобщающим медиатором, он реализует уточняющий спецификационный класс через уточняемый.
Медиаторный класс, указанный после ключевого слова down, называется уточняющим медиатором, он реализует уточняемый спецификационный класс через уточняющий.
Спецификационный класс может уточнять несколько спецификационных классов, при этом имена обобщающих медиаторов должны быть различны.
В объявлении спецификационного метода (см. раздел Спецификационные методы) может присутствовать ключевое слово refines, после которого следует список, каждый элемент которого является либо именем обобщающего медиатора, либо ключевым словом super, если наследуется функциональность совпадающего по сигнатуре спецификационного метода базового класса (см. раздел Наследование спецификационных классов).
SE_ClassRefinement ::= "refines" ClassOrInterfaceType "up" ClassOrInterfaceType "down" ClassOrInterfaceType ;
// импортирование вспомогательного класса ArrayList import java.util.ArrayList; // объявление спецификационного класса ListSpecification specification class ListSpecification { // объявление спецификационной модели данных public ArrayList items; // объявление спецификационного метода add, // описывающего операцию, добавляющую элемент в список в i-ую позицию specification void add(Object obj, int i) { ... } // объявление спецификационного метода get, // описывающего операцию, возвращающую i-ый элемент списка specification Object get(int i) { ... } // объявление спецификационного метода remove, // описывающего операцию, удаляющую i-ый элемент списка и // возвращающую удаленный элемент specification Object remove(int i) { ... } // объявление спецификационного метода size, // описывающего операцию, возвращающую размер списка specification int size() { ... } }
Ниже приводится объявление спецификационного класса StringListSpecification, описывающего список строк и уточняющего спецификационный класс ListSpecification. В нем присутствуют и другие спецификационные методы, но они переиспользуют уже имеющиеся спецификации.
// импортирование вспомогательного класса ArrayList import java.util.ArrayList; // объявление спецификационного класса StringListSpecification specification 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 void add(String obj, int i) refines StringListToList { post { return true; } } specification void addFirst(String obj) refines StringListToList { post { return true; } } specification void addLast(String obj) refines StringListToList { post { return true; } } specification String get(int i) refines StringListToList { post { return true; } } specification String remove(int i) refines StringListToList { post { return true; } } specification int size() refines StringListToList { post { return true; } } }
Ниже приводится объявление обобщающего медиатора StringListToList.
// объявление обобщающего медиатора StringListToList mediator class StringListToList implements StringListSpecification { // объявление реализационной ссылки на объект // спецификационного класса ListSpecification implementation ListSpecification l; // объявление медиаторных методов mediator void add(String obj, int i) { l.add(obj, i); } mediator void addFirst(String obj) { l.add(obj, 0); } mediator void addLast(String obj) { l.add(obj, l.size()); } mediator String get(int i) { return (String)l.get(i); } mediator String remove(int i) { return (String)l.remove(i); } mediator int size() { return l.size(); } }
Ниже приводится объявление уточняющего медиатора ListToStringList.
// импортирование вспомогательного класса ArrayList import java.util.ArrayList; // объявление уточняющего медиатора ListToStringList mediator class ListToStringList implements ListSpecification { // объявление реализационной ссылки на объект // спецификационного класса StringListSpecification implementation StringListSpecification l; // объявление медиаторных методов mediator void add(Object obj, int i) { l.add((String)obj, i); } mediator Object get(int i) { return l.get(i); } mediator Object remove(int i) { return l.remove(i); } mediator int size() { return l.size(); } // объявление блока синхронизации состояний update { items = (ArrayList)l.items.clone(); } }
Медиаторы предназначены для
связывания спецификации (см. раздел Спецификации) с
целевой системой или со спецификацией
другого уровня абстракции.
В дальнейшем для удобства изложения под
целевой системой будем понимать либо
непосредственно целевую систему, либо
спецификацию другого уровня абстракции.
Медиаторы решают следующие задачи:
Медиаторные классы предназначены для реализации медиаторов.
Каждый медиаторный класс связывает спецификационный класс (см. раздел Спецификационные классы) с некоторым компонентом целевой системы или со спецификационным классом другого уровня абстракции.
Медиаторные классы помечаются модификатором mediator, который указывается в самом начале их объявления.
Медиаторные классы наследуются от спецификационных или медиаторных классов и перегружают все или часть спецификационных методов (см. раздел Спецификационные методы), реализуя описанное в них поведение через обращения к операциям целевой системы.
Методы медиаторного класса, перегружающие спецификационные методы, называются медиаторными методами.
При вызове у объекта медиаторного класса спецификационного метода, не перегруженного никаким медиаторным методом, будет выполнено тело спецификационного метода, если оно определено.
В медиаторном классе могут определяться поля, содержащие ссылки на объекты целевой системы. Такие поля помечаются модификатором implementation и называются реализационными ссылками (см. раздел Реализационные ссылки).
SE_MediatorClassDeclaration ::= SE_ClassModifiers "mediator" UnmodifiedClassHeader SE_MediatorClassBody ; UnmodifiedClassHeader ::= "class" Identifier ( TypeParameters )? ( Super )? ( Interfaces )? ; SE_MediatorClassBody ::= "{" ( SE_MediatorClassBodyDeclaration )* "}" ; SE_MediatorClassBodyDeclaration ::= ClassBodyDeclaration | SE_ImplementationFieldDeclaration | SE_ImplementationInitializer | SE_MediatorMethodDeclaration | SE_ReactionMediatorMethodDeclaration | SE_UpdateBlockDeclaration ;
// объявление спецификационного класса AccountSpecification specification class AccountSpecification { static public int maximumCredit; public int balance; // объявление спецификационного метода deposit specification void deposit(int sum) { ... } // объявление спецификационного метода withdraw specification int withdraw(int sum) { ... } ... }
Ниже приводится объявление медиаторного класса AccountMediator, наследующего спецификационный класс AccountSpecification и перегружающего спецификационные методы deposit и withdraw.
// импортирование целевого класса Account import target.Account; // объявление медиаторного класса AccountMediator, // наследующего спецификационный класс AccountSpecification mediator class AccountMediator implements AccountSpecification { // реализационная ссылка на объект целевого класса implementation Account target = new Account(); // объявление медиаторного метода deposit mediator void deposit(int sum) { // вызов целевого метода deposit target.deposit(sum); } // объявление медиаторного метода withdraw mediator int withdraw(int sum) { // вызов целевого метода withdraw return target.withdraw(sum); } // объявление блока синхронизаций состояний объектов update { balance = target.balance; } // объявление блока синхронизаций состояний классов static update { maximumCredit = target.maximumCredit; } }
Реализационные ссылки являются специальными полями медиаторных классов (см. раздел Медиаторные классы) и предназначены для хранения ссылок на объекты целевой системы.
Реализационные ссылки используются для автоматической генерации статического метода create , создающего объект данного медиаторного класса (см. раздел Медиаторные классы).
Объявление реализационных ссылок отличается от объявления обычных полей добавлением в начало объявления модификатора implementation.
SE_ImplementationFieldDeclaration ::= ( Annotation )* "implementation" UnmodifiedFieldDeclaration ; UnmodifiedFieldDeclaration ::= Type VariableDeclarators ";" ;
// импортирование целевого класса Queue import target.Queue; // объявление медиаторного класса QueueMediator, // наследующего спецификационный класс QueueSpecification mediator class QueueMediator implements QueueSpecification { // объявление реализационной ссылки targetObject // на объект целевого класса Queue implementation Queue targetObject = null; ... }
SE_MediatorMethodDeclaration ::= ( SE_CommonModifier | "synchronized" | "final" )* "mediator" MethodHeader MethodBody ;
Используется для выделения обращений к реализации в медиаторах.
SE_ImplementationStatement ::= "implementation" ( Throws )? Statement ;
SE_UpdateStatement ::= "update" ( "[" ( SE_InvocationResultStorage )? MethodInvocation "]" )? Statement ;
SE_UpdateBlockDeclaration ::= ( "static" | "strictfp" | Annotation )* "update" Block ;
Реализационно-зависимые инициализаторы предназначены для описания действий, инициализирующих объекты целевой системы, доступные через реализационные ссылки (см. раздел Реализационные ссылки) медиаторных классов (см. раздел Медиаторные классы).
Реализационно-зависимые инициализаторы объявляются в медиаторных классах в блоках инициализации, помеченных ключевым словом implementation.
Выполнение реализационно-зависимых инициализаторов, объявленных в одном медиаторном классе, осуществляется в статическом методе create этого класса после создания объекта медиаторного класса и присваивания значений параметров метода реализационным ссылкам созданного объекта. Порядок выполнения инициализаторов совпадает с порядком их объявления.
SE_ImplementationInitializer ::= "implementation" Block ;
Ниже приводится фрагмент объявления целевого класса Account.
// объявление пакета target package target; // объявление целевого класса Account public class Account { // объявление поля balance public int balance; ... }
Ниже приводится фрагмент объявления медиаторного класса AccountMediator, наследующего спецификационный класс AccountSpecification (см. раздел Медиаторные классы) и осуществляющего инициализацию поля balance объекта целевого класса Account в реализационно-зависимом инициализаторе.
// импортирование целевого класса import target.Account; // объявление медиаторного класса AccountMediator mediator class AccountMediator implements AccountSpecification { // реализационная ссылка на объект целевого класса implementation Account targetObject = null; // реализационно-зависимый инициализатор implementation { targetObject.balance = 0; } ... }
Тестовые сценарии описывают тестовую последовательность (то есть последовательность обращений к операциям целевой системы), выполнение которой обеспечивает решение некоторой задачи тестирования.
Обычно в качестве такой задачи выступает тестирование некоторого набора операций целевой системы для достижения заданного уровня тестового покрытия (см. раздел Описание тестового покрытия).
Сценарные классы предназначены для задания тестовых сценариев, то есть для описания тестовой последовательности, выполнение которой обеспечивает решение некоторой задачи тестирования.
Сценарные классы помечается модификатором scenario, который указывается в их объявлении после всех других модификаторов и до ключевого слова class.
Внутри сценарных классов могут находиться объявления полей данных и методов.
Сценарные классы являются неявными наследниками класса jatva.lang.FormalScenario, который в свою очередь наследуется от java.lang.Thread, поэтому их можно использовать в качестве потоков: вызов метода start() в объекте сценарного класса запускает в отдельном потоке выполнение соответсвующего сценария.
В классе jatva.lang.FormalScenario определены следующие методы:
В сценарном классе могут объявляться сценарные методы и блок вычисления обобщённого состояния (см. разделы Сценарные методы и Блок вычисления обобщённого состояния).
SE_ScenarioClassDeclaration ::= SE_ClassModifiers "scenario" UnmodifiedClassHeader SE_ScenarioClassBody ; UnmodifiedClassHeader ::= "class" Identifier ( TypeParameters )? ( Super )? ( Interfaces )? ; SE_ScenarioClassBody ::= "{" ( SE_ScenarioClassBodyDeclaration )* "}" ; SE_ScenarioClassBodyDeclaration ::= ClassBodyDeclaration | SE_ScenarioMethodDeclaration | SE_ScenarioStateBlock ;
// объявление спецификационного класса SqrtSpecification specification class SqrtSpecification { // объявление статического спецификационного метода sqrt, // описывающего извлечение квадратного корня specification double sqrt(double x) { ... } }
Ниже приводится объявление сценарного класса SqrtScenario, использующего спецификационный класс SqrtSpecification.
// объявление сценарного класса SqrtScenario scenario class SqrtScenario { public double largeNumber = 1.0e15D; public int numberOfTrials = 5; // объявление конструкора сценарного класса SqrtScenario public SqrtScenario(int p_number) { SqrtSpecification.attachClassOracle(); numberOfTrials = p_number; } // объявление сценарного метода sqrt scenario sqrt() { iterate(int i = 0; i < numberOfTrials; i++) { choice { { execute SqrtSpecification.sqrt(i/largeNumber/numberOfTrials); } { execute SqrtSpecification.sqrt(1+i*largeNumber/numberOfTrials); } { execute 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) { } } }
Сценарные методы предназначены для описания набора обращений к целевой системе, которые необходимо осуществить в каждом обобщенном состоянии, достижимом во время тестирования (см. раздел Обобщенное состояние документа JavaTESK. Руководство пользователя).
Они также могут производить проверку корректности поведения вызываемых операций целевой системы.
Сценарные методы представляются как методы сценарного класса, не имеющие параметров, помеченные модификатором scenario и возвращающие результат типа boolean: true – если проверка показывает, что целевая система ведет себя корректно, false – иначе.
В сценарных методах для описания набора обращений к целевой системе можно использовать следующие конструкции:
SE_ScenarioMethodDeclaration ::= ( "strictfp" | "final" | Annotation )* "scenario" Identifier "(" ")" Block ;
При проверках, связанных с перегрузкой методов при наследовании, сценарные методы рассматриваются аналогично обычным Java-методам с типом возвращаемого значения boolean и пустым списком параметров.
// объявление сценарного метода sqrt scenario 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; }
SE_ExecuteStatement ::= "execute" Statement ;
// объявление сценарного класса BarrierTestScenario scenario class BarrierTestScenario { public BarrierSpecification barrier; // объявление сценарного метода deposit scenario waitCall() { if( barrier.awaitedThreads > 0 ) { // старт тестового фрема execute barrier.waitCall(); } return true; } }
Итерационные циклы предназначены для записи перебора значений параметров обращений к операциям целевой системы в сценарных методах (см. раздел Сценарные методы).
Синтаксис итерационного цикла языка JavaTESK похож на синтаксис цикла for(;;) языка Java. Объявление начинается с ключевого слова iterate, после которого в скобках через ; указаны:
Все указанные части, за исключением первой, являются необязательными и могут быть опущены. Объявление заканчивается телом итерационного цикла – итерационным блоком. Несмотря на сходство в записи итерационного цикла и цикла for(;;), итерационные циклы всегда выполняются хотя бы один раз, если выполнено условие фильтрации.
Итерационный цикл:
iterate(<объявление и инициализация итерационной переменной>
;<условие продолжение итерации>
;<шаг итерации>
;<условие фильтрации>
)
<итерационный блок>
подобен циклу:
<объявление и инициализация итерационной переменной>; do { if(<условие фильтрации>) <итерационный блок>; <шаг итерации>; } while(<условие продолжение итерации>);
Итерационные переменные, то есть переменные, значения которых перебираются в итерационном цикле, не являются обычными переменными, значения которых теряются при выходе из сценарного метода. Их значения запоминаются в специальной структуре данных, связанной с текущим обобщенным состоянием (см. раздел Обобщенное состояние документа J@T. Руководство пользователя). Эти значения становятся доступными, как только тест перейдет в данное обобщенное состояние снова.
Итерационные переменные являются частным случаем переменных обобщенного состояния (см. раздел Переменные обобщенного состояния).
SE_Iterate ::= "iterate" "(" Type VariableDeclarator ";" Expression ";" ( ForUpdate )? ( ";" ( Expression )? )? ")" Statement ; ForUpdate ::= StatementExpressionList ; StatementExpressionList ::= StatementExpression ( "," StatementExpression )* ;
// объявление сценарного класса AccountTestScenario scenario class AccountTestScenario { // объявление сценарного метода deposit scenario 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; } ... }
SE_CollectionIterate ::= "iterate" "(" Type Identifier ":" Expression ( ";" ( Expression )? )? ")" Statement ;
// объявление сценарного класса StoreTestScenario scenario class StoreTestScenario { // ссылка на модель товарного склада public StoreSpecification target; // список наименований товаров public ArrayList<String> goods; // максимальное количество едениц товара в каждом заказе public int maxAmountToOrder = 5; scenario order() { iterate(String goodsName : goods) { iterate(int amount = 1; amount<=maxAmountToOrder; amount++) { target.order(goodsName, amount); } } } }
SE_CoverageIterate ::= ( "casual" )? // not supported yet "coverage" ( "[" SE_CoverageSpecifier "]" )? ":" ( SE_Iterate | SE_CollectionIterate ) ; SE_CoverageSpecifier ::= SE_IntegralTypeCoverageSpecifier | SE_ExpressionCoverageSpecifier ; SE_IntegralTypeCoverageSpecifier ::= Expression "," Expression ; SE_ExpressionCoverageSpecifier ::= Expression ;
Определение: iterate-блоки, вложенные в SE_CoverageIterate и содержащие в себе инструкцию фильтрации, называются нанизанными.
Нанизанные iterate-блоки образуют цепочку от coverage iterate до инструкцию фильтрации.
SE_ExpressionFilterStatement ::= "filter" "[" Expression "]" ";" ;
SE_MethodInvocationFilterStatement ::= "filter" ":" ( SE_InvocationResultStorage )? MethodInvocation ";" ; SE_InvocationResultStorage ::= SE_VariableDeclarationResultStorage | SE_AssignmentResultStorage ; SE_VariableDeclarationResultStorage ::= VariableModifiers Type VariableDeclaratorId "=" ; SE_AssignmentResultStorage ::= ExpressionName AssignmentOperator ;
// объявление сценарного класса IntSetTestScenario scenario class IntSetTestScenario { // ссылка на модель множества целых чисел public IntSetSpecification objectUnderTest; // максимальное количество элементов в целевом множестве public int maximumNumberOfItems = 5; // объявление сценарного метода remove scenario remove() { // начало итерации данных // фильтрация будет производиться по покрытию маркированных путей coverage["mark"]: iterate(int i = 0; i < maximumNumberOfItems; i++) { // инструкция фильтрации по элементам покрытия метода remove filter: objectUnderTest.remove(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 class AccountTestScenario { public AccountSpecification target; // объявление сценарного метода deposit scenario deposit() { if(target.balance < 10) { // комбинатор выбора, описывающего перебор двух вызовов: // target.deposit(1) и target.deposit(5) choice { { target.deposit(1); } { target.deposit(5); } } } // дополнительных проверок не производится return true; } // объявление сценарного метода withdraw scenario 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 addAndRemove() { // объявление комбинатора сериализации serialize { // описание множества цепочек для сериализации { target.add(1); target.add(1); target.remove(1); } { target.remove(2); target.add(2); target.remove(2); } } // дополнительных проверок не производится return true; }
Переменные обобщенного состояния предназначены для хранения данных, связанных с обобщенным состоянием (см. раздел Обобщенное состояние документа J@T. Руководство пользователя). Их значения запоминаются в специальной структуре данных, связанной с текущим обобщенным состоянием, и становятся доступными, как только тест перейдет в него снова.
Объявление переменных обобщенного состояния начинается с модификатора state, после которого следует объявление переменных.
Код вида:
<оператор1>; state int i = 0; <оператор2>;
эквивалентен следующему (см. раздел Итерационные циклы):
<оператор1>; iterate(int i = 0;;) { <оператор2>; break; }
SE_StateVariableDeclaration ::= "state" Type VariableDeclarators ";" ;
// объявление сценарного метода fibbonachi scenario fibbonachi() { // объявление переменных обобщенного состояния state int f1 = 0; state int f2 = 1; // итерационный цикл, генерирующий последовательность из // первых десяти чисел Фиббоначи iterate(int i = 1; i <= 10; i++) { f2 = f2 + f1; f1 = f2 – f1; target.method(f1); } return true; }
SE_ScenarioStateBlock ::= ( "strictfp" | Annotation )* "state" Block ;
// объявление сценарного класса AccountTestScenario scenario class AccountTestScenario { public AccountSpecification target; // объявление блока вычисления обобщённого состояния state { return new Integer( target.balance ); } ... }
SE_CheckedPreStatement ::= "pre" "[" ( SE_InvocationResultStorage )? MethodInvocation "]" ( ( ":" Statement ) | ";" ) ;
Спецификации реакций предназначены для описания обратного интерфейса /*to change*/ теструемых компонентов. Обратный интерфейс /*to change*/ компонента - это набор операций, наличия которых он требует в своем окружении, и которые он может вызывать в ходе своей работы. Обратный интерфейс /*to change*/ состоит из реакций. Спецификация реакции определяет требования к функциональности этой реакции со стороны компонента, использующего его.
Стоит отметить, что требования к методу со стороны использующего его компонента могут отличаться от контракта этого метода в одном из реализующих его компонентов. В согласованной системе первое является следствием второго. Точнее, постусловие спецификации реакции должно быть следствием постусловия соответствующего стимула, а предусловие спецификации реакции должно влечь предусловие стимула.
При моделировании сложного поведения с помощью API реакция может представлять любой выделенный вид воздействий, оказываемых тестируемым компонентом на свое окружение. Это может быть операция, вызываемая тестируемым компонентом, или событие, создаваемое им. Если вызовы операций самого тестируемого компонента приходится моделировать в виде пар событий обращение-возврат управления, то возврат управления моделируется с помощью специальной спецификации реакции.
Спецификация реакции, так же, как и спецификация обычного метода, состоит из общего блока, пред- и постусловия. Выделяется она ключевыми словами reaction specification.
SE_ReactionSpecification ::= ( SE_CommonModifier | "synchronized" )* "reaction" "specification" SE_MethodHeader SE_MethodBody ;
Классы-медиаторы реакций являются классами объектов, помещаемых в тестируемую систему для мониторинга инициируемых ею событий. С точки зрения моделирования объект такого класса отслеживает определенного рода события в тестируемой системе и переводит их в вызовы реакций на уровне модели.
Классы-медиаторы реакций должны определять ряд методов, в коде которых происходят обращения к реакциям. Такие методы называются методами-медиаторами реакций. В их рамках обращения к модельным реакциям производится либо простым вызовом реакции как java-метода, либо - в случае, если есть необходимость синхронизации модельного состояния с реализационным, - при помощи оператора update, имеющего квадратные скобки.
Помимо обращений к реакциям класс-медиатор реакций может определять зависящие от тестируемой реализации действия по синхронизации модельного состояния.
SE_ReactionMediatorClassDeclaration ::= SE_ClassModifiers "reaction" "mediator" UnmodifiedClassHeader SE_ReactionMediatorClassBody ; SE_ReactionMediatorClassBody ::= "{" ( SE_ReactionMediatorClassBodyDeclaration )* "}" ; SE_ReactionMediatorClassBodyDeclaration ::= ClassBodyDeclaration | SE_ReactionMediatorMethodDeclaration | SE_UpdateBlockDeclaration ;
SE_ReactionMediatorMethodDeclaration ::= ( SE_CommonModifier | "synchronized" | "final" )* "reaction" "mediator" MethodHeader MethodBody ;
// метод-медиатор реакций, реализующий выходной канал для // сервера чата с отдельным логическим выходным каналом для каждого клиента // здесь подразумевается, что каждому клиенту чата соответствует отдельный поток, воспринимающий // сообщения, посылаемые сервером этому клиенту ChatSpecification cs; reaction mediator void acceptMessage( ChatMessage m ) { if( m instanceof ErrorMessage ) cs.errorSend( m.getDestination(), m.getErrorCode() ); else if( m instanceof TextMessage ) cs.textSend( m.getDestination(), m.getText() ); }
Данная конструкция перенаправляет все модельные события, зарегистрированные при выполнении текущего потока от начала вложенного блока до его конца, в канал, указанный в заголовке конструкции. Для "возвращения" модельных событий в канал по умолчанию - то есть в канал, связанный с текущим потоком, - нужно использовать в качестве идентификатора канала ключевое слово default.
Нужно иметь ввиду, что если результат выражения-идентификатора канала равен null, то переключения событий в другой канал происходить не будет.
SE_ChannelizeEventsStatement ::= "<:" ( Expression | "default" ) ":>" Block ;
Никаких семантических ограничений на данную конструкцию не накладывается, так же как и, например, на вызовы спецификационных методов.
// метод-медиатор реакций для сервера чата, обладающим единственным // каналом передачи выходных сообщений // все сообщения, посланные сервером чата, воспринимаются одним и тем же потоком ChatSpecification cs; reaction mediator void sendMessage( byte[] chatMessageData ) { ChatMessage cm = Utils.parseChatMessage( chatMessageData ); <: cm.getClientID() :> { // вызов обратного медиаторного метода из // раздела Методы-медиаторы реакций acceptMessage( cm ); } }
При возникновении тех или иных ошибок во время работы теста JavaTESK автоматически определяет набор данных, относящихся к этой ошибке. Эти данные попадают в отчёт о тестировании на страницу описания ошибки. Но иногда бывает желательно либо дополнить эти данные, либо же - представить их в более удобном виде.
Данная конструкция даёт возможность автору теста задать собственный комментарий к ошибкам теста или тестируемой системы. Этот комментарий будет отображаться на странице отчёта, посвящённой соответствующей ошибке. Прокомментировать можно лишь некоторые виды ошибок, а именно ошибки, возникающие при невыполнении вердиктов компонентов теста: сценарных методов, инвариантов, а также пред- и постусловий спецификационных операций.
Вердикт задаётся первым выражением, а комментарий, вычисляемый в случае отрицательного вердикта, - во втором.
SE_ReturnStatement ::= "return" Expression ":" Expression ";" ;
reaction specification void sendNotSubscribed( String destClientID ) { LinkedList<OutgoingMessage> expectedMessages = null; pre { expectedMessages = messagesToSend.get( destClientID ); if( expectedMessages == null ) return false; return ( expectedMessages.size() == 1 && expectedMessages.get( 0 ) == notSubscribed ) : "NotSubscribed message must be sent to " + destClientID ; } }
Иногда бывает нужно в сценарии ожидать появления той или иной реакции. Это требуется в тестах систем, обладающих сложным поведением в промежуточных состояниях (не стационарных). Например, судить о том, в какое промежуточное состояние перешла система после первого стимула, можно только по тому, какая появилась реакция и появилась ли она вообще. Таким образом от выданных реакций зависит допустимость подачи следующих стимулов, т.к. разные стимулы можно подавать в разных промежуточных состояниях.
Если сценарию по тем или иным причинам требуется дождаться появления некоторых модельных событий, то можно использовать специальную инструкцию "ожидания".
Инструкция ожидания событий задаёт максимальное время ожидания, описывает свойства событий, при появлении которых ожидание прекращается, а также может определять наборы действий, которые нужно выполнить после появления событий с теми или иными свойствами. Для описания свойств ожидаемых событий могут используоваться паттерны модельных событий.
Одновременно в состоянии ожидания появления реакций могут находиться сразу несколько потоков, контролируемых тестовой системой. Те потоки, для паттернов которых нашлось подходящее событие, разблокируются и продолжают свою работу. Одно событие может разблокировать ожидания нескольких потоков.
Самый типичный use-case этой инструкции - ожидание реакции на стимул. Однако конструкцию "ожидания" можно использовать более широко: во-первых, ожидать не только реакции, но и стимулы (подданные другими сценарными потоками); во-вторых, ожидание не только с момента подачи стимула, но и с любого момента времени, в том числе - с момента начала фрейма.
Для того, чтобы встать в блокирующее ожидание событий, сценарный поток должен:
Свойства ожидаемых событий можно задавать как с помощью описанной ниже синтаксической конструкции, так и самостоятельно создавая объект-паттерн, реализующий определённый в библиотеке интерфейс.
Смысл предварительной инициации в определении момента времени, начиная с которого новые появляющиеся события будут проверяться относительно паттернов. Для текущего сценарного потока создаётся очередь, которая будет заполняться новыми событиями. Именно эта очередь будет просматриваться в пункте 4.
Подача стимула должна произойти полностью, то есть до начала блокировки (просмотра очереди) управление должно вернуться в сценарий.
Сценарный поток начинает просматривать события, зарегистрированные в тестовой системе.
SE_ExpectInitializeStatement ::= "expect" "new" ";" SE_ExpectEventStatement ::= SE_ExpectEventAfterStimulusStatement | SE_GeneralExpectEventStatement ; SE_ExpectEventAfterStimulusStatement ::= "do" "[" MethodInvocation "]" "expect" ( "for" "[" Expression "]" )? "{" ( SE_EventExpectationElement )+ "}" ; SE_GeneralExpectEventStatement ::= "expect" ( "new" )? ( "for" "[" Expression "]" )? "{" ( SE_EventExpectationElement )+ "}" ; SE_EventExpectationElement ::= ( SE_StopExpectSelector )+ ( BlockStatement )* ; SE_StopExpectSelector ::= "case" Expression ":" | "timeout" ":" ;
Выражение, написанное в квадратных скобках после for, задаёт время ожидания появления реакций и называется выражением-таймаутом.
Инструкция ожидания состоит из заголовка и набор альтернатив - действий, которые нужно предпринять,, если произошло то или иное событие. Каждая альтернатива содержит описания таких событий (SE_StopExpectSelector) и список действий (BlockStatement), которые нужно предпринять, если произошло одно из событий этой альтернативы.
Тест проверяет корректность совокупности событий. Событиями могут быть как действия, контролируемые тестом (стимулы), та к и действия, наблюдаемые тестом (реакции). Выражения-паттерны модельных событий предназначены для компактного определения предикатов над событиями, регистрируемыми тестовой системой. Предикат, определяемый выражением-паттерном, строится как коньюнкция сравнений значений атрибутов реально случившегося модельного события с эталонными значениями тех же атрибутов, заданными в паттерне.
Факт регистрации события оформляется в тесте как вызов спецификационной операции - стимула или реакции соответственно. Таким образом, для модельного события определены следующие атрибуты:
Для стимулов также определены атрибуты "возвращаемое значение" и "возникшее исключение", но на данный момент выражения-паттерны не позволяют задавать эталонные значения этих атрибутов.
Для каждого аргумента модельного события можно указать его тип (частично определив сигнатуру) или же непосредственное значение. Runtime тип аргумента события НЕ является атрибутом события.
Если паттерны используются в качестве селекторов причин окончания ожидания, то на позициях аргументов с неизвестными значениями можно декларировать свободные переменные, в которые будут записаны значения аргументов реально случившихся событий. Эти свободные переменные можно будет использовать в действиях, предусмотренных альтернативами инструкции ожидания.
SE_EventPatternExpression ::= "event" ( Primary | AmbiguousName )? "#" ( NonWildTypeArguments )? <ID> ( "<:" Expression ":>" )? "(" ( SE_PatternArgumentList )? ")" ; SE_PatternArgumentList ::= SE_PatternArgument ( "," SE_PatternArgument )* ; SE_PatternArgument ::= Type ( "..." )? ( VariableDeclaratorId )? | Expression ;
Выражение-паттерн может описывать свойства разных модельных событий (например, задав значение только одного из нескольких аргументов). Но все модельные события, описываемые одним выражением-паттерном, должны являться вызовами одной и той же модельной операции. Требование существования хотя бы одной операции гарантирует, что нельзя задать паттерн, которому не может соответствовать ни одно модельное событие. Требование единственности модельной операции продиктовано сложностями статического анализа.