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

{Л V КГС УТ>) (АТС) V {ATI)) V (BTC) V {BTV) {АТВ)к{АТС) {ЛГВ к С) А{АТВУВ) {АТВ & -В).

К правилам вывода добавляется правило экстенциональности: если эквивалентность некоторых формул доказана, то они взаимозаменяемы.

Время в этой темпоральной логике дискретное; это линейное течение исчислимых последовательных случаев. Если число полных состояний мира равно 2", то число возможных историй в т последовательных моментах равно 2""* [45, с.80-81].

3.5.4. Приложение временных логик к программированию

Пусть а - программа, ф - высказывание, относящееся к входным данным, которое должно быть истинно перед выполнением программы а, и 9t - высказывание, которое должно быть истинно после выполнения программы а. Высказывание ф называется предусловием, а 9t - постусловием программы а ®.

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

{Щат.

Программа а называется тотально правильной по отношению к ф и 9t, если она частично правильна по отношению к ф и 9t, и

Проведем аналогию с модальными (временными) логиками: каждое состояние памяти, возникающее при выполнении программы, аналогично «возможному миру» в семантике Крипке; пути выполнения программы определяют переходы между этими мирами [22, с.75].

обязательно завершает работу, если ф истинно®. В этом случае используется запись

{Ща i {Щ.

Предусловие ф и постусловие 9t связаны с конкретной задачей, которую требуется решить и для решения которой и написана программа а. Нам важно доказать, что она правильна!

Проверка того, что программа действительно выполняет задачи, дпя решения которых она создавалась, - это задачи тестирования и верификации программы.

Для решения задачи верификации программы используются временные логики.

Основные идеи приложения временных логик к программированию сводятся к следующим двум положениям [22, с.146):

1. Огшсание программ. С помощью языка временной логики, специализированного особым образом, выразить свойства программ, характеризующих их правильное вычислительное поведение.

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

Одно из первых упоминаний идеи доказательства правильности программ содержится в статье Дж. Маккарти (1961): «Вместо того, чтобы испытывать программы до тех пор, пока они не окажутся отлаженными, нужно доказывать, что они имеют желаемые свойства». К этому же времени относится выступление Э. Дейкстры с докладом «Некоторые соображения о более развитом программировании».

Впервые (1974) мысль об использовании логических временных знаков «всегда» и «иногда» для верификации программ проявилась в статье Р.Вурсталла [49]. Однако речь шла о последовательных программах, представляющих собой один вычислительный процесс. Временные верификации программ в полной мере развились по отношению к параллельным программам, т.е. программам, состоящим из нескольких процессов, работающих одновременно и взаимодействующих между собой.

® Исполнение а обязательно завершается, и 9t должно быть истинно в любом состоянии памяти ЭВМ, которое может получиться при выполнении а. Это соответствует □ 9t (необходимо 9t) в модальной логике [22, с. 75].

3.5.5. Временная логика Пнуели

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

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

Таким образом, логика Пнуели предназначена для верификации программ, связанных с параллельными вычислениями.

Временная логика Пнуели строится как логика первого порядка с прибавлением множества новых пропозициональных переменных вида аЫ, которые пробегают по выражениям вида «процесс Pi находится в метке /». Это дает средства для описания контрольного компонента программных состояний. Кроме того, переменные языка разбиваются на два типа: глобальные переменные и локальные переменные.

Глобальные переменные не меняют своих значений от состояния к состоянию, а значения локальных переменных меняются.

Логика Пнуели содержит дополнительные знаки F (когда-нибудь будет), G (всегда будет) и i< (в следующий момент будет) и аксиомы: