Android-приложение для поиска дешевых авиабилетов: play.google.com
Главная -> Классическая логика

0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 [22] 23 24 25 26 27 28 29 30 31 32 33

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

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 + г)}. Доказательство

Язык

Метаязык

вывод

2l=>n=n + m*0

в формальной арифметике

{п = п + m * 0}г := п{п = г + m * 0}

аксиома Al

{п = г + m* 0}g := 0{п = г + т*д}

аксиома Al

{Щг .= п{п = г + т*0}

AS к пунктам 1 и 2

{21}г .= n;q:= 0{п = г + т*д}

А4 к пунктом 3 и 4

п = г + m*g&i

арифметика

&m <= г => п = (г - m) + m * (g + 1)

{п = (г - т) + т* (q + 1)}г := г - m {n = r + m*(g+l)}

аксиома Al

{n = + m * (g + l)}g := g + 1

аксиома Al

{n = r + m*g}

{n = (r - m) + m * (q + l)}r := r - m;

АА к пунктам 7 и 8

g := g+ l{n = r + m* g}

{n = + m * g&m <= r}r .= r -m; g := g +l{n = r+ m* g}

А2 к пунктам 6 и 9

{n = r + m* q&an <= r}while m <= r do beqin r := r - m; g := g + 1 end

{(n = r + m* g)&-i(m <= r)}

А8 к пункту 10

{ЩЗ{{п = r +m* g)&-(m <= r)}

АА к пунктам 5 и 11 ч.т.д.

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

1) т <= г;

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

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

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

msim.

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



0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 [22] 23 24 25 26 27 28 29 30 31 32 33



0.0124
Яндекс.Метрика