Итерация по покрытиям

Нацеленная итерация Одно обобщённое воздействие на каждый элемент некоторого покрытия. Элементы покрытия перебираются по порядку. Для каждого фиксированного элемента подбираются конкретные данные для воздействия.

Итерация по элементам покрытия с функцией вычисления Покрытие Внутри сценарного метода –Конструкцию iterate coverage Способ подбора конкретных данных. Точку проверки попадания в требуемый элемент. Действия, которые нужно выполнить, если мы попали в нужный элемент.

Пример 1 extern coverage IntCoverage( int i ) = { POSITIVE, ZERO, NEGATIVE }; scenario bool s() { iterate coverage IntCoverage { int j = -2; for( ; j < 2; j ++ ) filter IntCoverage( j ) { abs_impl( j ); } } Итерация по элементам глобального вычислимого покрытия.

Пример 2 extern coverage IntCoverage( int i ) = { POSITIVE, ZERO, NEGATIVE }; specification void f( int x, int y ) coverage C = IntCoverage( x ) * IntCoverage( y ) ; // in scenario iterate coverage f.C { for( int x = -3; x

Пример 2 Определение стимула. extern coverage IntCoverage( int i ) = { POSITIVE, ZERO, NEGATIVE }; extern coverage f.C( int x, int y ) = IntCoverage( x ) * IntCoverage( y ); specification void f( int x, int y ); // in.sec specification void f( int x, int y ) { pre {... } coverage C; post {... } }

Итерация по «константным» покрытиям Покрытие Внутри сценарного метода –Конструкцию iterate coverage Способ подбора конкретных данных для некоторого элемента. Действия, которые нужно выполнить.

Пример 3 extern coverage Reqs = { REQ_1, REQ_2, REQ_3 }; scenario bool s() { iterate coverage Reqs { int j; switch( r ) { case Reqs.REQ_1: case Reqs.REQ_2: j = -1; break; case Reqs.REQ_3: j = 2 ; break; } filter Reqs { abs_impl( j ); } } Итерация по элементам глобального константного покрытия.