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

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