Д.ARMоед (05.12.2011 14:06, просмотров: 140) ответил Evgeny_CD на Не понял. Если граф перехода КА синзезирован в виде функции, и она синтезирована на С правильно (реентерабельная, работает только с локальными переменными, все, что передается ей - RO, она возврашает либо стандартно, либо в спецальную структуру,
"Скрипач не нужен"(с) В том смысле, что из процесса вообще можно исключить сишные либы и тулчейны. Поскольку изначально верифицировать сишные либы формальными методами низзя. Можно только проверить на предмет наличия известных ошибок. А вот машину Тьюринга в примере выше - можно. Можно даже олтмоделировать посредством xslt-шаблонов - тоже формально верифицируемых. Конечно, чтобы вырастить народ способный сразу записать это дело в xml-е, понадобится время. Но никто не мешает перегнать эвентбишное описание в xml с помощью того же самого xslt. Насчёт верилога выше была почти шутка потому что последний не всегда формализуется до такой степени, как EventB.
Получается, что в сухом остатке имеем все формально верифицируемые ступени проектирования.
p.s.: Можно сгенерить сишные либы описанным способом, гарантирующим от side-effect, и дать их народу - "бултыхайтесь, типа..".