пользователей: 30398
предметов: 12406
вопросов: 234839
Конспект-online
РЕГИСТРАЦИЯ ЭКСКУРСИЯ

Логика Пнуели и алгоритмические логики.

Алгоритмическая логика (или динамическая логика, или программная логика, или логика Хоара) — раздел теоретического программирования, в рамках которого исследуются аксиоматические системы, представляющие средства для задания синтаксиса и семантики языков программирования, а также для синтеза компьютерных программ и их верификации (проверки правильности работы). Языки алгоритмических логик основываются на логике предикатов 1-го порядка и включают в себя высказывания вида \{A\}S\{B\}, читающиеся следующим образом: "Если до исполнения оператора S было выполнено A, то после него будет выполнено B". Здесь A называется предусловием, B — постусловием, либо обещанием S. На этом языке даются логические описания операторов присвоения и условного перехода, ветвления, цикла.

 

Наряду с динамической логикой 1-го порядка рассматривается пропозициональная динамическая логика и ее обобщение — так называемая логика процессов, в которой выразимы некоторые свойства программы, зависящие от процесса ее выполнения. Различные динамические логики получаются при варьировании средств языков программирования, используемых в программах. Эти средства содержат массивы и другие структуры данных, рекурсивные процедуры, циклические конструкции, а также средства задания недетерминированных программ.

 

Динамическая логика является одним из типов логических систем, используемых для логического синтеза компьютерных программ. Логический синтез — один из способов перехода от спецификации программы к реализующему алгоритму, имеющий форму точного рассуждения в некоторой логической системе. В динамической логике спецификация задачи задается в виде двух формул исчисления предикатов — предусловия и постусловия, а аксиомами логической системы являются схемы предусловий и постусловий, связываемых теми или иными конструкциями языка программирования. Синтезируемая программа получается в форме выводимого в динамической логике утверждения, гласящего, что если аргументы задачи удовлетворяют заданному предусловию, то результат выполнения синтезированной программы удовлетворяет заданному постусловию.

 

В теоретических работах по динамическим логикам исследуются вопросы непротиворечивости и полноты аксиоматических систем, алгоритмические сложностные свойства множеств истинных формул, сравнения выразительной мощности языков динамической логики.

 

Принципиально иной способ определения семантики программ, пригодный, скорее для описания всего алгоритмического языка, а не конкретных программ, предложил в 1970 г. американский логик Д. Скотт. Он построил математическую модель λ-исчисления и показал, как переводить функциональное описание языка структурного программирования в λ-исчисление и как определить математическую модель алгоритмического языка через модель λ-исчисления. Эта так называемая денотационная семантика алгоритмических языков, работы по которой насчитываются уже тысячами, стала практическим инструментом построения надежных трансляторов со сложных алгоритмических языков. Так еще одна абстрактная область математической логики нашла прямые практические приложения.

Временная логика Пнуели
Темпоральная логика Пнуели создана с целью верификации ком-
пьютерных программ. Другими словами, логика Пнуели - это фор-
мальная теория, с помощью которой молено доказывать «наличие
у данной программы свойств, характеризующих ее правильное вы-
числительное поведение»/

Приведем рассуждения Пнуели по этому поводу: «...Нужно ли
понятие внешнего времени, или темпоральности, для рассуждений
о программах?... для последовательных программ темпоральность
не является существенной. Это так потому, что эти программы име-
ют «внутренние часы», а именно само выполнение. Зная метку в
программе и значения программных переменных, мы можем точ-
но определить, в каком месте выполнения мы находимся. Поэтому
для таких программ простые временные понятия «до» и «после»
выполнения программного сегмента ... адекватны. Но при обраще-
нии к программам индетерминистским, параллельным, в которых
выполнение состоит из перемешанных между собой операций из
различных процессов, мы должны различать «где» и «когда» и со-
хранять внешнюю временную шкалу, независимую от выполнения»

Таким образом, логика Пнуели предназначена для верификации
программ, связанных с параллельными вычислениями.
Временная логика Пнуели строится как логика первого порядка
с прибавлением множества новых пропозициональных переменных
вида atl, которые пробегают по выражениям вида «процесс Р{ на-
ходится в метке I». Это дает средства для описания контрольного
компонента программных состояний. Кроме того, переменные язы-
ка разбиваются на два типа: глобальные переменные и локальные
переменные.
Глобальные переменные не меняют своих значений от состояния
к состоянию, а значения локальных переменных меняются.
Логика Пнуели содержит дополнительные знаки F (когда-
нибудь будет), G (всегда будет) и N (в следующий момент будет) и
аксиомы:

G(A->B)->(GA->GB)

N(A->B)->(NA->NB)

GA->A

GA->NGA

GA->NA

NнеA=-неNA

(A&G(A->NA))->GA

Дополнительное правило вывода:
(A\GA)
В данной логике устанавливается инвариантное правило, гласящее,
что для того, чтобы установить инвариантность (неизменность) некоторого свойства А в данной программе, надо установить: а) оно имеет место в начале
программы и б) сохраняется после выполнения каждой команды этой программы.

 


23.01.2014; 09:37
хиты: 0
рейтинг:0
для добавления комментариев необходимо авторизироваться.
  Copyright © 2013-2024. All Rights Reserved. помощь