Корныхин Евгений ВМК МГУ Система генерации тестовых программ с использованием ограничений ТЕСЛА
Абстрактная форма тестовой программы Тестовая программа ТЕСЛА тестирование уточнение
Тестовый шаблон : ADD x, y, z 0 LD u, x, cacheHit DIV y, u, divBy MOV y, XXX SD XXX
REGISTER rt, rs, rd, ru: 32; … ADD rt, rs, overflow LD ru, rt, normal(cacheMiss) VAR x,y,z: 32; t y[31]||y + z[31]||z; ASSERT t[32] != t[31]; VAR x: 32; … addr y + z; x Load(addr); тестовый шаблон описания тестовых ситуаций overflow.tslnormal.tsl