9.5. Пример доказательства свойства программы.

На основании доказанных правил верификации программ можно доказывать свойства программ, состоящих из операторов присваивания и пустых операторов и использующих три основные композиции структурного программирования. Для этого, анализируя структуру программы и используя заданные ее пред- и постусловия, необходимо на каждом шаге анализа применять подходящее правило верификации. В случае применения композиции повторения потребуется подобрать подходящий инвариант цикла.

В качестве примера докажем свойство (9.4). Это доказательство будет состоять из следующих шагов.

(Шаг 1). n>0  (n>0, p  любое, m  любое).

(Шаг 2). Имеет место

{n>0, p  любое, m  любое} p:=1 {n>0, p=1, m  любое}.

 По теореме 9.2.

(Шаг 3). Имеет место

{n>0, p=1, m  любое} m:=1 {n>0, p=1, m=1}.

 По теореме 9.2.

(Шаг 4). Имеет место

{n>0, p  любое, m  любое} p:=1; m:=1 {n>0, p=1, m=1}.

 По теореме 9.3 в силу результатов шагов 2 и 3.

Докажем, что предикат p= m! является инвариантом цикла, т.е. {p=m!} m:=m+1; p:=pm {p=m!}.

(Шаг 5). Имеет место {p= m!} m:= m+1 {p= (m1)!}.

 По теореме 9.2, если представить предусловие в виде {p= ((m+1)1)!}.

(Шаг 6). Имеет место {p= (m1)!} p:= pm {p= m!}.

 По теореме 9.2, если представить предусловие в виде {pm= m!}.

(Шаг 7). Имеет место инвариант цикл

{p= m!} m:= m+1; p:= pm {p= m!}.

 По теореме 9.3 в силу результатов шагов 5 и 6.

(Шаг 8). Имеет место

{n>0, p=1, m=1} ПОКА m <> n ДЕЛАТЬ

m:= m+1; p:= pm

ВСЕ ПОКА {p= n!}.

 По теореме 9.6 в силу результата шага 7 и имея в виду, что (n>0, p=1, m= 1)  p= m!; (p= m!, m= n)  p= n!.

(Шаг 9). Имеет место

{n>0, p  любое, m  любое} p:=1; m:=1;

ПОКА m <> n ДЕЛАТЬ

m:= m+1; p:= pm

ВСЕ ПОКА {p= n!}.

 По теореме 9.3 в силу результатов шагов 3 и 8.

(Шаг 10). Имеет место свойство (9.4) по теореме 9.5 в силу результатов шагов 1 и 9.

Упражнения к лекции 9.

9.1. Что такое триада Хоора?

9.2. Что такое свойство программы?

9.3. Пусть заданы описания

const n= <конкретное целое значение>;

var k, m: integer;

x: array[1..n] of integer;

Доказать свойство программы:

{n>0}

m:= x[1]

k:=1;

ПОКА k<n ДЕЛАТЬ

k:= k+1;

ЕСЛИ x[k]<m ТО

m:= x[k]

ВСЕ ЕСЛИ

ВСЕ ПОКА;

{n>0 & m<= x[i] для всех i, 1<=i<= n}

Литература к лекции 9.

9.1. С.А. Абрамов. Элементы программирования. - М.: Наука, 1982. С. 85-94.

9.2. М. Зелковец, А. Шоу, Дж. Гэннон. Принципы разработки программного обеспечения. - М.: Мир, 1982. С. 98-105.