Логика невзаимодействующих программ и реактивных систем

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