Моделирование
Для формального задания модели целевого языка используется представление грамматики языка в форме BNF.
Модель синтаксиса целевого языка задается в виде формального описания на языке TreeDL [] структуры корректных абстрактных синтаксических деревьев целевого языка.
Модель статической семантики целевого языка задается в виде списка контекстных условий. Для их формального описания используется язык SRL (Semantic Relation Language), специально разработанный для этой цели [].
Модель структуры входных данных задается в виде формального описания на языке TreeDL [].
Требования к программному интерфейсу формализуются как контрактные спецификации. Такой подход к спецификации основан на представлении об описываемой системе как наборе компонентов, взаимодействующих с окружением и между собой. Контрактная спецификация состоит из модельного состояния, которое моделирует внутреннее состояние системы поддержки исполнения, и набора спецификационных функций. Спецификационные функции формализуют требования к обработке входящих и исходящих функциональных вызовов посредством логических выражений в постусловиях. Такой подход к спецификации программных интерфейсов близок к логике Т. Хоара и концепции «проектирования на основе контрактов» Б. Майера.
Формальные спецификации программного интерфейса записываются на расширении языков программирования Си [] или Java []. Из формальных спецификаций автоматически генерируются тестовые оракулы - процедуры, которые выносят вердикт о соответствии наблюдаемого поведения системы спецификации.
