G{A В) {GA GB) ЩАВ) {iAm) GAA

GA mA

GAViA iA =

{AkG(A K))GA Дополнительное правило вывода:

В данной логике устанавливается инвариантное правило, гласящее, что

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

Символически это правило записывается как

В А, atl&cB (для всех меток I) BGA

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

О чем идет речь? В параллельных вычислениях параллельные процессы могут включать блоки (секции), содержащие команды, критические дпя кооперирования этих процессов. Иначе говоря, пока один процесс находится в своей критической секции и выполняет команды этой секции, второй процесс не должен войти в свою критическую секцию, поскольку изменения в ячейках памяти, происходящие при выполнении команд идущего первого процесса, исказят вычисления, на которые сориентирован второй процесс. Второй процесс должен ждать,пока содержимое используемых им ячеек

Для этого требуется понятие «внешнего времени».

не окажется требуемым. Ожидание происходит в силу выполнения особых команд программы, называемых семафорными инструкциями.

Рассмотрим пример семафорной инструкции [22, с.148-149].

Пример 3.1. В параллельной программе имеются две критические секции (КС). Семафорная инструкция - оператор «wait ... then...» с семафорной переменной 0:4:

Xi := 1;

Предположим, что при выполнении процесса 1 значение Xi уменьшилось до 0. Тогда компьютер вынужден остановить процесс 2, т.к. преградой к его выполнению является семафорная инструкция под меткой TOq, для выполнения которой необходимо, чтобы Xi было больше 0. Следовательно, компьютер начнет выполнять команды с метками h - la и только после этого перейдет к продолжению выполнения процесса 2. Другими словами, пока процесс 1 находится в своей критической секции КС1, процесс 2 не достигнет своей критической секции КС2. То же самое будет происходить в случае, когда процесс 2 начнет выполняться первым.

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

\- G{athk...&i.atln),

(3.12)

где li - метка критической секции г-го процесса, Л - формула, выражающая исходные условия*.

Формальное доказательство теоремы (3.12) дано в [22, с.152-155].

Исходные условия включают в себя значения программных переменных, предусловие (если оно имеется) и исходные метки всех параллельных процессов программы.

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

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

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

msm,

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

Эти логические языки практически одновременно изобретены Р.У.Флойдом (1967), К.Хоаром (1969) и представителями польской логической школы (А.Сальвиницкий и др. (1970)).

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

В 70-х годах на базе работы Хоара начинаются исследования в области аксиоматических определений языков программирования. Появляется много работ по аксиоматизации различных конструкций: от оператора присваивания до различных форм циклов, от вызовов процедур до сопрограмм. Главным упущением исследователей в эти годь! является то, что они уделяли недостаточно внимания формальной логике.

В 1972 году вышла очередная статья Хоара о доказательстве правильности представления данных, что ускорило исследования по абстрактным типам данных. В СССР работы в этой области велись в Новосибирске (А.П.Ершов, В.Н.Агафонов, А.В.Замулин, И.Н.Скопина).

В 1973 году были сформулированы правила доказательства правильности для большинства конструкций языка Паскаль. В 1975 была построена автоматическая система верификации для подмножества языка Паскаль, основанная на аксиомах и правилах вывода. В 1979 году был Определен язык программирования Евклид, в проект которого с самого начала была заложена идея аксиоматизации.

В 1976 году (в русском переводе в 1978 году) вышла книга Э.Дейкстры «Дисциплина программирования», в которой нредпа-гается метод доказательства правильности программ. Суть мето-