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

Пусть α – программа, b – высказывание, относящееся к входным данным, которое должно быть истинно перед выполнением программы α,и – высказывание, которое должно быть истинно после выполнения программы α. Высказывание b называется предусловием, а – постусловием программы α.

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

{b} α {}

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

{} α↓ {}

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

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

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

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

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

Алгоритмические логики

В начале 70-х годов XX века возникли алгоритмические логики. Они создавались с целью описания семантики языков программирования.

Алгоритмические логики включают высказывания вида

{b} S {}

читающиеся как «если до выполнения оператора S было выполнено b, то после него будет .

Принципы построения алгоритмической логики

Опишем принципы построения алгоритмической логики L₀.

Память в L₀ разделена на ячейки. Каждая ячейка имеет идентификатор, представляющий собой слово из латинских букв и цифр и начинающийся с буквы. Ячейки содержат натуральные числа.

Программа в L₀ состоит из операторов. Исходный оператор присваивание:

х:=е,

где х – идентификатор, а е – выражение, составленное из идентификаторов и натуральных чисел.

Пусть состояние памяти после присваивания удовлетворяет условию A(х), где А – формула формальной арифметики. Тогда состояние, которое было до присваивания, опишем формулой A(х|е). Иначе говоря, имеем высказывание

{A(х|е)}х := е{A(х)}.

Например, если A(х) – это x < 2 и х := х + 1, то A(х|х+1) – это x + 1 < 2. Следовательно, чтобы после присваивания х := х + 1 стало истинным x < 2, требуется, чтобы до присваивания выполнялось неравенство x + 1 < 2, т.е.

{x + 1 < 2} х := х + 1 {x < 2}.

Пусть два оператора S₁, S₂ выполняются один за другим. Тогда этому соответствует логическая запись вида

Условный оператор – это конструкция

IF A₁→ S₁ ∆ A₂→ S₂ ∆ ... ∆ A_n→ S_n FI,

где A₁,..., A_n – логические выражения, построенные из отношений e₁ = e₂, e₁ > e₂ при помощи логических связок; S_i – последовательность операторов. Проверяются формулы A_i при настоящем состоянии памяти. Если ни одна из A_i не истинна, то фиксируется ошибка. Если же некоторые A_i истинны, то выбирается одна их них (неважно как) и выполняется соответствующая последовательность операторов S_i.

Если каждая из команд S_i описана в логике L₀ как {A_i}S_i{B}, то условный оператор описывается логической формулой

{(A₁A₁)^…^(A_nA_n)} IF A₁→ S₁ ∆ A₂→ S₂ ∆ ... ∆ A_n→ S_n FI {B}.

Циклам отвечает конструкция

DO A₁→ S₁ ∆ ... ∆ A_n→ S_n OUT B₁→ T₁ ∆ ... ∆ B_m→ T_m OD

При выполнении оператора цикла проверяются формулы A₁,…, A_n, B₁,…, B_m при настоящем состоянии памяти. Если ни одна из них не истинна, то фиксируется ошибка. Если же некоторые истинны, то выбирается одна из них (неважно как). Если выбрана A_i, то выполняется соответствующая последовательность операторов S_i и выполнение цикла возобновляется. Если выбрана В_i, то выполняется соответствующая последовательность операторов Т_i и выполнение цикла завершается.