Шаг 4. Доказательство истинности составленных условий корректности

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

Возможности доказательства условий корректности U_a зависят от проблемной области.

Пример

Доказать частичную корректность программы вычисления частного и остатка от деления целых чисел xи y.

Программа на Паскале:

r := x; q := 0;

while y £ r do

begin r := r – y; q := q + 1 end

Блок-схема этой программы имеет вид:

1. Разрезание цикла программы.

Разрежем цикл программы в точке входа в цикл (точка t₃)..

2. Получение аннотированной программы.

Запишем индуктивные утверждения для программы в контрольных точках t₁, t₂ и t₃.

P: inv_t1( x,y ) º ( x ³ 0 ) Ù ( y > 0 );– условие корректных исходных данных

Q: inv_t2 ( x,y, q,r ) º ( x = r + y*q ) Ù ( r < y ); –условие выхода из цикла

inv_t3 ( x,y, q,r ) : x = r + y*q– инвариант цикла.

3. Определение набора условий корректности для всех путей между соседними контрольными точками программы.

Путями между контрольными точками являются:

Таким образом, доказана истинность всех трех условий корректности и. следовательно, установлено свойство частичной корректности программы.

Пример 2

Доказать частичную корректность программы вычисления z = [Öx]для любого целого x ³ 0. [Öx]есть наибольшее целое число k такое, что k £ Öx.

Решение

Метод вычисления, на котором основана программа, основывается на известном соотношении: 1 + 3 + 5 + … + (2k + 1) = (k + 1)² для каждого k ³ 0.

Пусть значение суммы запоминается в s, а нечетные числа 2k + 1 –в n.

Программа на Паскале:

k := 0; s:= 0; n:= 1;

s := s + n;

while x £ s do

begin k := k +1; n := n + 2;

s := s + n;

end;

z := k;

Блок-схема этой программы имеет вид:

1. Разрежем цикл программы в точке B.

2. Получение аннотированной программы.

Запишем индуктивные утверждения для программы в контрольных точках A, B и C.

P: inv_A(x) º x³0 ;– условие корректных входных данных

Q: inv_С ( x,z ) º (z² £ x) Ù ( x < (z+1)² ); –условие выхода из цикла

inv_B (x,k, s,n): ( k²£x ) Ù ( s= (k+1)² ) Ù ( n=2k+1 )– инвариант цикла.

Определение набора условий корректности для всех путей между

соседними контрольными точками программы.

Путями между контрольными точками являются:

выражение( x ³ 0 ) Þ ( ( 0² £ x ) Ù (1 = 1) Ù (1 = 1) ) º

(x ³ 0) Þ (0 £ x) º Ø(x ³ 0) Ú (0 £ x) º (x < 0) Ú (x ³ 0) º true

4.2. Преобразуем условие U_a2.

( k² £ x ) Ù ( s = (k+1)² ) Ù ( n=2k+1 ) Þ ( (s £ x) Þ

( (k+1)² £ x ) Ù ( s + n +2 = (k+2)² ) Ù ( (n+2) = 2( k+1) +1) ) º

( ( k² £ x ) Ù ( s = (k+1)² ) Ù ( n=2k+1 ) Ù (s £ x) ) Þ

( (k+1)² £ x ) Ù ( s + n +2 = (k+2)² ) Ù ( (n+2) = 2( k+1) +1) )

Для доказательства истинности условия U_a2 нужно показать, что соотношения, образующие конъюктивные члены справа от знака импликации, следуют из соотношений, стоящих слева от знака импликации.

а) Поскольку x ³ sи s = (k+1)², то (k+1)² £ x.

б) s+n+2 = (k+1)² + 2k + 1 + 2 º k² + 2k+ 1+ 2k + 1 + 2 = (k+2)²

в) n+2 = 2 (k+1) +2 = 2 (k+1)+1

Следовательно, условие истинно.

4.3. Преобразуем условие U_a3.

( k² £ x ) Ù ( s = (k+1)² ) Ù ( n=2k+1 ) Þ ( ( s > x ) Þ

(k² £ x) Ù ( x < (k+1)² ) º

( k² £ x ) Ù ( s = (k+1)² ) Ù ( n=2k+1 ) Ù ( s > x ) Þ

(k² £ x) Ù ( x < (k+1)² )

Поскольку s > xи s = (k+1)², то (k+1)² > xи U_a3 – истина