Спецификация
Для решения задачи спецификации, генерации тестовых данных и оценки покрытия в качестве основы мы будем использовать технологию UniTESK [,]. В UniTESK проверка корректности производится на основе задания пред- и постусловий функций, а также инвариантов [,]. Дополнительно для обеспечения возможности спецификации параллельных и распределенных систем введено понятие отложенной реакции [], с помощью которых удается моделировать внутренний недетерминизм в системе. Для рассмотренного примера приведенные ограничения на систему могут быть сформулированы в виде инвариантов на состояние (Рис. 7). В модельном состоянии theCompanies хранятся описания компаний: статус компании и информация о родителях. Инвариант Rule1_InactiveParent проверяет первое ограничение, а Rule2_Level4Hierachy - второе. invariant Rule1_InactiveParent() { for (Company company: theCompanies) { if (company.isActive()) { if (company.parent!=null && !company.parent.isActive()) return false; } } return true; } invariant Rule2_Level4Hierarchy() { for (Company company: theCompanies) { if (company.computeLevel()>4) return false; } return true; }
Рис. 7. Спецификация ограничений
