компьютерных наук королева Великобритании пожаловала Хоару рыцарское звание.

3.6.3. Алгоритмическая логика Хоара

Основой для логики выводов правильных программ служат аксиомы Хоара (правила верификации). Они допускают интерпретации в терминах программных конструкций.

Сформулируем аксиомы Хоара, которые определяют предусловия как достаточные условия, гарантирующие, что исполнение соответствующего оператора при успешном завершении приведет к

желаемым постусловиям .

Al. Аксиома присваивания:

{Щх\е)}х := е{Щ.

Неформальное объяснение аксиомы: так как х после выполнения будет содержать значение е, то 9t будет истинно после выполнения, если результат подстановки е вместо ж в 9t истинен перед выполнением.

А2. msm & (?j $к) {i3}s{fK}. A3, msm & ($к £2) {щзт-

Пусть S - это последовательность из двух операторов Si, Si (составной оператор).

АА {£i}Si{j & m}S2m тз{щ.

Очевидно, что это правило можно сформулировать для последовательности, состоящей из п операторов.

Сформулируем правило для условного оператора (краткая форма):

А5. {£I&«B}Si{fK}&(£I&-«B «R) {£I}if «В then Si{«R}.

Аксиома АЬ соответствует интерпретации условного оператора в языке программирования.

Сформулируем правило для альтернативного оператора (полная форма условного оператора):

A6.({£I&«B}Si{«R})&({£I&-«B}S2{$R}){£2}if«BthenSielseS2{$R}.

и для операторов цикла.

Использованы материалы сайта http: stud.math.rsu.ru/deikstra/.

Предусловия и постусловия цикла until (до) удовлетворяют правилу:

А7. {£2&<B}Si{£2} {£2}repeat Si until <В{£2&-«В}.

Правило вводит важное понятие инварианта цикла. Предикат £2, истинный перед выполнением и после выполнения каждого шага цикла, называется инвариантным отношением или просто инвариантом цикла. В математике термин «инвариантный» означает не изменяющийся под воздействием совокупности рассматриваемых математических операций. В данном случае единственная операция - это выполнение шага цикла при условии истинности £2 вначале.

Предусловия и постусловия цикла while (пока) удовлетворяют правилу:

А8. {£2&«B}Si{£2} {£2}while «В do Si{£2&-«B}.

Аксиомы Al - А8 можно использовать для проверки согласованности передачи данных от оператора к оператору, для анализа структурных свойств текстов программ, для установления условий окончания цикла. Кроме того, правила можно использовать для анализа результатов выполнения программы, что связано с семантикой программы.

Пример 3.2. Пусть надо определить частное q и остаток г от деления п на т.

Входные данные:

п,т- целые неотрицательные числа, причем т> 0.

Выходные данные:

q,r - целые неотрицательные числа.

Описание программы S:

задать(п, т) г :=п; д:=0; while т <= г do

begin (3.13)

г :=r - т; д := д+1

end;

выдать(д, ?); Сформулируем предусловие 21:

т > 0&(n,m) - целые числа. Сформулируем постусловие 55:

(г < m)&(n = т*д + г).

Нужно доказать, что

N msm

\= {т> 0&(п, т) - целые} S {(г < m)&(n = m * g + г)}. Доказательство

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

1) т <= г;

2) г, g - неотрицательные целые числа.

Значение г на каждом шаге цикла уменьшается на положительную величину: г := г - m(m > 0). Значит, последовательность значений гид является конечной, т.е. найдется такое значение г, для которого не будет выполняться условие т <= г, и циклический процесс завершится.

Таким образом, установлено, что

msim.

Иначе говоря, наша программа S является тотально правильной.