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

Еще мне интересна сама постановка задачи доказательства правильности систем по аналогии доказательства правильности программ. Можно построить по аналогии с программированием. Спецификацией системы будет формальное описание требований. А реализацией - какой-то проект/план/модель будущей системы. Соответственно, нужно доказать, что реализация соответствует формальным требованиям. В (псевдо)математической нотации: Допустим, A - сигнатура модели (грубо говоря, формальное описание входов/выходов, типа A : In -> Out), Req(a) - предикат, заданный на множестве этих сигнатур. В другой форме, Req(in, out). Предикат задает требования, т.е. те сигнатуры, на которых предикат выполним, являются корректными реализациями. Соответственно, задача проверки корректности требований, состоит в том, чтобы доказать, что Exists a : A, Req(a). В другой форме Exists f : In->Out, Forall x, Req(x, f(x)). Если доказательство, конструктивное, то по нему можно извлечь и саму модель, отвечающую требованиям. Но на практике, модель нужно разрабатывать отдельно, потому как в целях удобство доказывания, модель должна иметь структуру, отличную от той, которую нужно применять в реальности (грубо говоря, экономить нужно другие ресурсы). И потом доказывать, что сия модель соответствует спецификации. Соответственно, возникают три подзадачи: 1. формальное задание сигнатуры целевой системы (тип преобразования входов в выходы) 2. построение предиката задающего требования (например, бинарный предикат на парах вход/выход) 3. построение модели целевой системы, имеющей нужную сигнатуру, и доказательство, того, что модель соответствует требованиям Все это довольно сложно и трудоемко, но на практике, даже простенькие частичные формализации часто весьма полезны для понимания требований.