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

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