Здравствуйте, Аноним, Вы писали:

А>Спасибо Всем кто откликнулся на предыдущий зов!

А>Однако всё же несколько вопросов остались не рассмотренными.

А>2) Формальные спецификации?
А>Допустим, написаны OCL ограничения как их работать с ними дальше? Возможно ли их сохранить в каком-либо формате, а затем передать в автоматизированную среду тестирования? Напишите ссылки на среды разработки формальных спецификаций (RSL, SDL, ...)

Я более-менее подробно смотрел только PVS (читал пару туториалов, не более). Идея в следующем: написать спецификации, а затем смотреть, что из них получается — выводить теоремы и т.п. Предназначена для нахождения дыр в самих спецификациях.

А>3) Да есть системы доказательства корректности (Isabelle, HOL, Coq). Можно ли их где нибудь скачать?
А в чем проблема? Coq, HOL, Isabelle. И вообще, вот.