AtelierB - от спецификации до генерации кода. Код генерируется AtelierB, у нас имеется генератор для С, С++ и Ада. Знающие наверное догадались - в основе этого лежит метод B (предшественник Z). В основе всего этого лежит логика предикатов, теория множеств и так далее. Вот тут немного теории http://stud.math.rsu.ru/deikstra/4.htm
В начале дается математическая модель поставленной задачи (MACHINE), затем она рафинируется (RAFINEMENT), то есть конкретизируем эту мат. модель. Так вот, к концу этой цепочки конкретизации, мы пишем нашу начальную мат. модель на языке B0 (как любой другой язык прог-я, тока он для AtelierB). На протяжении всего рафинирования AtelierB следит чтобы каждое звено цепи соответсвовало мат. модели. Если это доказанно, то остается тока выбрать язык на котором будет сгенерирован код. И никаких тестов на не надо делать! Скомпилировал и пользуйся.
На screen-shot виднеется мат. модел графа, определения что такое наикратчайший путь между двума узлами графа и так далее. Зеленый свет означает че мат. модель доказанна! ;)
официальный сайт Ателёр Б http://www.atelierb.societe.com/index_uk.html
результаты использования http://www.atelierb.societe.com/PAGE_B//uk/ref-01.htm
>>> Просмотр (1280x1024, 218 Kb)
