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

3.6.1. Принципы построения

алгоритмической логики

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

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

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

X := е,

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

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

{Л{х\е]}х :=е{Л{х)}.

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

{Щ81{Ъ}, {€}82т, {2l}SiS2{S)}

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

IF Л1 - Si А Л2 - 82А ... АЛп8п FI,

Использованы материалы сайта http: stud.math.rsu.ru/deikstra/. К примеру, если А(х) - это ж < 2 и ж := ж -- 1, то А(х\х -- 1) -это ж -I- 1 < 2. Следовательно, чтобы после присваивания ж := ж -- 1 стало истинным ж < 2, требуется, чтобы до присваивания выполнялось неравенство х + 1 < 2, т.е. {ж --1 < 2}ж := х + 1{ж < 2}.

где Л1, ...An - логические выражения, построенные из отношений ei = 62,61 > 62 при помош;и логических связок; Si - последовательность операторов. Проверяются формулы Ai при настояш;ем состоянии памяти. Если ни одна из Ai не истинна, то фиксируется ошибка. Если же некоторые Ai истинны, то выбирается одна их них (неважно как) и выполняется соответствуюш;ая последовательность операторов Si.

Если каждая из команд Si описана в логике Lo как {2li}Si{55}, то условный оператор описывается логической формулой

{{А, 2li)&...&(A. 21„)}IF Л, - Si Д Л2 - S2 А ...

... AAnSn FI{<B}.

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

DO Л1 - Si Д ... Д Л„ - S„ OUT Bl - Tl Д ... АВтТт OD.

Выполняется оператор цикла следуюш;им образом. Проверяются формулы Al,An,Bi, ...,Вт при настояш;ем состоянии памяти. Если ни одна из них не истинна, то фиксируется ошибка. Если же некоторые истинны, то выбирается одна их них (неважно как). Если выбрана Ai, то выполняется соответствуюш;ая последовательность операторов Si и выполнение цикла возобновляется. Если выбрана Bi, то выполняется соответствуюш;ая последовательность операторов Ti и выполнение цикла завершается.

Если каждая из команд Si описана в логике Lo как {2li}Sj{£i}, а Ti как {S)i}Tj{*Bi}, то однократное выполнение цикла описывается логической формулой

{(Л1 Щк...к{Ап 2l„)&(Bi !Di)k...k{Bm S)m)&

k{Ai V ... V Л„ V Bl V ... V Вт)} IFAi -Si A ... AAnSn A

ABlTlA ... ABmTm FI{<B}.

Двукратное выполнение цикла дает формулу

{(Л1 2li)&...&(„ 2l„)&(Bi S)i)&...&(Bm S)m)&

&(Л1 V ... V Л„ V Bl V ... V Вт)} ITAi -SiA...AAnSnA Д Bl Tl Д ... АВтТт FI{€i V ... V €п} {{Al 2li)&...&(„ 2l„)&(Bi S)i)&...&(B™ S)m)&

&(€! V ... V £„)&(л1 V ... V Л„ V Bl V ... V Вт)} IVAi Si А ... ... AAnSn ABiTi А ... ABruTru FI{<B}

и т.д. до бесконечности. Условие правильности к шагов цикла обозначим через DO*{*B}. Цикл корректен, если

Н DO{<B} V DO{<B} V ... V DO*{<B} V ...

Но это бесконечно длинная формула! Она не является формулой языка Lq. Появление таких формул - это серьезная проблема для алгоритмических логик.

3.6.2. Чарльз Хоар

Профессор Чарльз Хоар (Charles Antony Richard Hoare) родился в 1934 г. в Англии. В 1980 г. получил престижную премию Алана Тьюринга за вклад в формальное определение языков программирования посредством аксиоматической семантики. Хоар известен своими работами в области алгебры программ. Превращение программирования в серьезную профессиональную дисциплину стало ведущим мотивом ею научной деятельности

С начала 60-х годов профессор Хоар является ведущим ученым в мире в области компьютерных наук. В числе его заслуг - разработка логики Хоара (Ноаге

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

Рис. 3.3: Ч.А.Р. Хоар.

11 CM.http: www.vavilon.ra/koval/ruslaslov-01 .html

1Использована статья Anatem с сайта: http: www.ct.kz/