Без заголовка

Собственно в этом и различаются наши позиции. Относительно софта автор уже выразился в том смысле, что доказательство корректности работы программы (любой) можно провести, т.к. любая программа есть в пределе конечный автомат, для которого по определению можно построить как точный (бинарный) предикат, так и всевозможные его модельные приближения (в т.ч. с выделением существенных требований). По отношению к системам такого сказать к сожалению нельзя, т.к. например человеко-машинные системы уже конечным автоматом не являются (в силу наличия в них неопределенности, связанной с человеческим фактором). Опять же - ситуация с ограничениями. Практически гарантировано, если Вы начнете задавать ограничения методом отсечений (т.е. описывать слабоформализованные области, куда системе можно ходить, а куда нельзя) то Вы нарветесь на невыполнимый предикат гораздо раньше, чем сможете описать поведение системы с многочисленными обратными связями, внутренними состояниями и сложными переходами между ними, по крайней мере, если не захотите работать в пространстве, мерность которого равна суммарному количеству степеней свободы системы (которое при слабой формализации области может быть катастрофически велико для реальных систем). С этой сложностью неизбежно придется бороться структурными методами. Поэтому чисто предикативная методика, ИМХО, обречена именно потому, что с доказательством будут неразрешимые проблемы. Эти проблемы огребли по полной японцы, когда начали на Прологе пытаться сделать компьютер пятого поколения. Проект, насколько мне известно, загнулся, проглотив полмиллиарда баксов. Хотя ребят сложно обвинить в некомпетентности и в том, что они сознательно формулировали сложно верифицируемые формализмы. Кстати, и наши работы по ИИ (например, см. ВИНИТИ, работы В.К.Финна) говорят, что если начать работать все-таки со структурной информацией (графами) и использовать более гибкие системы рассуждений (т.н. правдоподобный вывод), то можно добиться куда большего, чем тупо пытаться соорудить предикат, описывающий систему. И к слову, чем Вас так не устраивает знание, которое получается в процессе правдоподобного вывода или рассуждений на графах, чем оно хуже предикативных утверждений? ИМХО, именно там и надо копаться в поисках приемлемого формализма, а не в предикатах, как таковых.