Тестирование функциональности, не зависящей от истории взаимодействия системы с окружением Занятие 3

Спецификации Генератор тестовой последовательности Спецификации Итератор тестовых воздействий Тестовый сценарий Медиаторы на SE C Целевая система Обходчик Оракул Медиатор Спецификации Разработка спецификаций Разработка медиаторов Разработка тестовых сценариев Шаги разработки теста в CTesK:

Спецификационная функция trunc_spec specification mix_num trunc_spec(mix_num* mn) { pre { return mn.denom > 0 && ( mn.integral >= 0 && mn.num >= 0 || mn.integral num)) denom) && *mn || mn->integral * mn->denom + mn->num ); } }

Спецификационная функция specification (,..., ) { pre {... } coverage {... } post {... } } сигнатура тело

Указатели в качестве параметров спецификационной функции specification f( int* i, int* iarray ) {... if(*i == 0) if(iarray[3] != 0) }

; * ; Спецификационные типы void* create(& _type,…); int compare(Object*,Object*); bool equal(Object*,Object*); void* copy(Object*,Object*); void* clone(Object*); String* toString(Object* ref) Integer, Double, Char, String, Set, List, Map

Определение спецификационного типа specification typedef = {.init = указатель_на_функцию_инициализации,.copy = указатель_на_функцию_копирования,.compare = указатель_на_функцию_сравнения,.to_string = указатель_на_функцию_преобразования_в_строку,.enumerator = указатель_на_функцию_перечисления_ссылок,.destroy = указатель_на_функцию_освобождающую_ресурсы }; specification typedef = {}; specification typedef ;

Cпецификационный тип MixNum int compare_MixNum(mix_num* left, mix_num* right) { int l = left->num * right->denom, r = right->num * left->denom; if(left->entire != 0) l += left->denom * left->entire; if(right->entire != 0) r += right->denom * right->entire; return l – r; } specification typedef mix_num MixNum = {.compare = compare_MixNum };

Сигнатура функции trunc_spec specification MixNum* trunc_spec(MixNum* mn);

Структура тела спецификационой функции specification ( ) { pre {... } coverage {... } post {... } }

pre { if(...) /* входные значения соответствуют требованиям предусловия */ return true; else return false; } specification (...) { pre { if(...) /* входные значения соответствуют требованиям предусловия */ return true; else return false; }... } Предусловие outputs ( *arg, result ) Целевая система call inputs ( arg, *arg )

Предусловие функции trunc_spec pre return mn->denum > 0 specification MixNum* trunc_spec(MixNum* mn) { pre { return mn->denum > 0 && ( mn->entire > 0 && mn->num > 0 && ( mn->entire > 0 && mn->num > 0 || mn->entire num entire num < 0 || mn->entire == 0 && mn->num == 0 ); || mn->entire == 0 && mn->num == 0 ); }... }

Инварианты типов /* invariant of C type */ invariant typedef ; invariant( value) { if(/* инвариант выполнен для значения value */) return true; else return false; } /* invariant of specification type */ invariant specification typedef = {...}; invariant( *r) {...}

invariant( value); invariant( value); specification ( * arg) { pre {...} coverage {...} post {...} } Автоматическая проверка инвариантов типов для значений параметров спецификационной функции outputs ( *arg, result ) Целевая система call inputs ( arg, *arg ) Пре-значения Пост-значения invariant(*arg); invariant(*arg); invariant( );

Инвариант спецификационного типа MixNum invariant specification typedef mix_num MixNum; invariant(MixNum* mn) { return mn.denum > 0 && ( mn.entire >= 0 && mn.num >= 0 || mn.entire entire == 0 && mn->num == 0 ); } pre return mn->denum >0 && ( mn->entire >= 0 && mn->num >= 0 || mn->entire num denum >0 && ( mn->entire >= 0 && mn->num >= 0 || mn->entire num entire == 0 && mn->num == 0 ); || mn->entire == 0 && mn->num == 0 ); }... }

Критерий покрытия coverage {... if(...) /* * при данных пре-значениях параметров покрывается данная ветвь */ return {, };... } specification (...) { pre {...} coverage {... if(...) /* * при данных пре-значениях параметров покрывается данная ветвь */ return {, };... } post {...} } outputs ( *arg, result ) Целевая система call inputs ( arg, *arg )

Полнота критерия покрытия coverage С { if(...) /* Условие 1 */ return { BRANCH_1, "1 st branch" }; else if(...) /* Условие 2 */... else return { LAST_BRANCH, "Last branch" }; } Любой набор пре-значений параметров должен соответствовать одной из ветвей функциональности критерия покрытия:

Критерий покрытия функции trunc_spec coverage С { if(mn->entire == 0 && mn->denum > mn->num) return {PROP_FRACT, "Proper fraction"}; if(mn->entire == 0 && mn->denum num) return {IMPROP_FRACT, "Improper fraction"}; if(mn->entire != 0 && mn->denum > mn->num) return {PROP_MIXED, "Proper mixed number"}; else /*(mn->entire != 0 && mn->denum num)*/ return {IMPROP_MIXED, "Improper mixed number"}; } specification MixNum* trunc_spec(MixNum* mn) { pre { return mn->denum > 0 && ( mn->entire >= 0 && mn->num >= 0 || mn->entire num entire == 0 && mn->denum > mn->num) return {PROP_FRACT, "Proper fraction"}; if(mn->entire == 0 && mn->denum num) return {IMPROP_FRACT, "Improper fraction"}; if(mn->entire != 0 && mn->denum > mn->num) return {PROP_MIXED, "Proper mixed number"}; else /*(mn->entire != 0 && mn->denum num)*/ return {IMPROP_MIXED, "Improper mixed number"}; }... }

Постусловие post { if(...) /* пост-значения удовлетворяют требованиям постусловия */ return true; else return false; } specification (...) { pre {...} coverage {... } post { if(...) /* пост-значения удовлетворяют требованиям постусловия */ return true; else return false; } } точка вызова outputs ( *arg, result ) Целевая система call inputs ( arg, *arg )

Доступ в постусловии к пре-значениям и значению возвращаемого результата specification int func(int *u) { post { != 0 && func == *u } } outputs ( *arg, result ) Целевая система call inputs ( arg, *arg )

Постусловие функции trunc_spec post { return trunc_spec->integral == mn->integral specification MixNum* trunc_spec(MixNum* mn) { pre { return mn != NULL; } coverage С { if(mn->entire == 0 && mn->denum > mn->num) return {PROP_FRACT, "Proper fraction"}; if(mn->entire == 0 && mn->denum num) return {IMPROP_FRACT, "Improper fraction"}; if(mn->entire != 0 && mn->denum > mn->num) return {PROP_MIXED, "Proper mixed number"}; if(mn->entire != 0 && mn->denum num) return {IMPROP_MIXED, "Improper mixed number"}; } post { return trunc_spec->integral == mn->integral && trunc_spec->denom == mn->denom && trunc_spec->denom == mn->denom && trunc_spec->num == mn->num && trunc_spec->num == mn->num && mn->denom && mn->denom && abs(mn->num) denom && abs(mn->num) denom && mn); && mn); } } }

Медиатор Медиаторы Генератор тестовой последовательности Спецификации Итератор тестовых воздействий Тестовый сценарий Медиаторы на SE C Целевая система Обходчик Оракул Медиаторы на SeC Разработка спецификаций Разработка медиаторов Разработка тестовых сценариев Шаги разработки теста в CTesK:

Определение медиаторов в SeC mediator for specification ( ) { call { /* map specification args to implementation ones */... if(.../* if something wrong */) setBadVerdict( ); /* implementation call */... /* map implementation results to specification ones */... if(.../* if something wrong */) setBadVerdict( ); return ; } }

Медиатор функции trunc_spec mediator trunc_media for specification MixNum* trunc_spec(MixNum* mn) { call { mix_num imn, res; imn.entire = mn->entire; imn.num = mn->num; imn.denom = mn->denom; res = trunc(&imn); mn->entire = imn.entire; mn->num = imn.num; mn->denom = imn.denom; return create(&MixNum_type, res.entire,res.num,res.denom); } }

Сценарии Генератор тестовой последовательности Спецификации Итератор тестовых воздействий Тестовый сценарий Медиаторы на SE C Целевая система Обходчик Оракул Медиатор Сценарий Разработка спецификаций Разработка медиаторов Разработка тестовых сценариев Шаги разработки теста в CTesK:

Определение сценария scenario dfsm = {.init =,.actions = {,..., NULL },.finish = } set_mediator_ ( );

Сценарные функции scenario bool () {... ( );... return ; }

Оператор iterate scenario bool () {... iterate( ; ; ; ) { }... return ; } =

Поток управления в сценарной функции scenario bool () {... iterate( ; ; ; ) {... }... return ; } Обходчик

Сценарий для функции trunc_spec bool trunc_scen_init (int argc, char **argv) { set_mediator_trunc_spec (trunc_media); return true; } scenario bool trunc_sf () { iterate (int i = -10; i = 0) iterate (int denom = 1; denom

Функция main, вызов сценария int main(int argc, char** argv) { ( argc, argv ); }

Функция main для теста функции trunc int main(int argc, char **argv) { trunc_scen(argc, argv); }