Шаг 4. Доказательство истинности составленных условий корректности
Введенное понятие условия Uaмежду соседними контрольными точками позволяет свести задачу анализа частичной корректности программы Prgm к доказательству истинности условий между любыми соседними контрольными точками программы Prgm.
Теорема (без док-ва). Программа Prgm частично корректна относительно предусловия P и постусловия Q, если для каждого пути a между соседними контрольными точками условие пути Ua истинно.
Важность этой теоремы состоит в том, что она позволяет абстрагироваться от конкретных процессов между соседними контрольными точками вычислений по программе и рассматривать только условия Ua между соседними контрольными точками, т.е. рассматривать только характеристики статической структуры программы.
Возможности доказательства условий корректности Ua зависят от проблемной области.
Пример
Доказать частичную корректность программы вычисления частного и остатка от деления целых чисел xи y.
Программа на Паскале:
r := x; q := 0;
while y £ r do
begin r := r – y; q := q + 1 end
Блок-схема этой программы имеет вид:
 |
1. Разрезание цикла программы.
Разрежем цикл программы в точке входа в цикл (точка t3)..
2. Получение аннотированной программы.
Запишем индуктивные утверждения для программы в контрольных точках t1, t2 и t3.
P: invt1( x,y ) º ( x ³ 0 ) Ù ( y > 0 );– условие корректных исходных данных
Q: invt2 ( x,y, q,r ) º ( x = r + y*q ) Ù ( r < y ); –условие выхода из цикла
invt3 ( x,y, q,r ) : x = r + y*q– инвариант цикла.
3. Определение набора условий корректности для всех путей между соседними контрольными точками программы.
Путями между контрольными точками являются:
a1 :от входа программы к началу цикла (t1 – t3);
a2 :от начала цикла через тело цикла обратно к началу цикла (t3 – t3);
a3 :от начала цикла через условие цикла к выходу программы (t3 – t2).
Тогда
Ua1 : P Þ invt3 ( r x, q 0 ) º
( x ³ 0 ) Ù ( y > 0 ) Þ x = x + y*0 º
( x ³ 0 ) Ù ( y > 0 ) Þ x = x º
( x ³ 0 ) Ù ( y > 0 ) Þ true
Ua2 : invt3 ( x,y, q,r ) Þ
( ( y £ r ) Þ invt3 ( x,y, q q+1, r r – y) ) º
(x = r + y*q ) Þ ( ( y £ r ) Þ ( x = ( r - y ) + y*(q + 1))) º (x = r + y*q ) Þ ( ( y £ r ) Þ (x = r + y*q ) );
Ua3 : invt3 ( x,y, q,r ) Þ ( ( y > r ) Þ Q ) º
(x = r + y * q ) Þ ( ( y > r ) Þ (x = r + y * q ) Ù ( r < y ) )
4. Доказательство истинности условий Ua.
Условие Ua1– истина, так как x1 Þ x2 – тождественная истина, еслиx2 – истина.
Преобразуем условие Ua2.
(x = r + y * q ) Þ ( ( y £ r ) Þ (x = r + y * q ) ) º
( (x = r + y * q ) Ù ( y £ r ) ) Þ (x = r + y * q ) ) º
Ø( (x = r + y * q ) Ù ( y £ r ) ) Ú ( x = r + y * q ) º
Ø( x = r + y * q ) Ú Ø( y £ r ) Ú ( x = r + y * q ) º
Ø( y £ r ) Ú true º ( y £ r ) Þ true.
Следовательно, Ua2 – истина (по аналогии с Ua1).
Преобразуем условие Ua3.
(x = r + y * q ) Þ ( ( y > r ) Þ (x = r + y * q ) Ù ( r < y ) ) º
(x = r + y * q ) Ù ( y > r ) Þ (x = r + y * q ) Ù ( r < y ) º
( y > r ) Þ ( r < y ), так как x = r + y * q– true.
Следовательно, Ua3 – истина
Таким образом, доказана истинность всех трех условий корректности и. следовательно, установлено свойство частичной корректности программы.
Пример 2
Доказать частичную корректность программы вычисления z = [Öx]для любого целого x ³ 0. [Öx]есть наибольшее целое число k такое, что k £ Öx.
Решение
Метод вычисления, на котором основана программа, основывается на известном соотношении: 1 + 3 + 5 + … + (2k + 1) = (k + 1)2 для каждого 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: invA(x) º x³0 ;– условие корректных входных данных
Q: invС ( x,z ) º (z2 £ x) Ù ( x < (z+1)2 ); –условие выхода из цикла
invB (x,k, s,n): ( k2£x ) Ù ( s= (k+1)2 ) Ù ( n=2k+1 )– инвариант цикла.
Определение набора условий корректности для всех путей между
соседними контрольными точками программы.
Путями между контрольными точками являются:
a1 :от входа программы к точке разреза цикла (A – B);
a2 :от точки разреза цикла через тело цикла обратно в точку разреза цикла (В – B);
a3 :от точки разреза цикла через условие цикла к выходу программы
(B – C).
Тогда
Ua1 : P Þ invB (x,k, s s+n,n) º
( x ³ 0 ) Þ (k2 £ x ) Ù ( s+n = (k+1)2 ) Ù ( n=2k+1 ) ) º
( x ³ 0 ) Þ ( 02 £ x ) Ù (0+1 = (0+1)2) Ù ( 1=2*0+1 ) ) º
( x ³ 0 ) Þ ( ( 02 £ x ) Ù (1 = 1) Ù (1 = 1) );
Ua2 : invB (x,k, s,n) Þ ((s£x) Þ
invB(x,k k+1, s s+n, n n+2)) º
( k2 £ x ) Ù ( s = (k+1)2 ) Ù ( n=2k+1 ) Þ ((s£ x) Þ
( (k+1)2 £ x ) Ù ( s + n +2 = (k+2)2 ) Ù ( (n+2) = 2*( k+1) +1) );
Ua3 : invB (x,k, s,n) Þ ( ( s £ x ) Þ invС ( x,z k) ) º
( k2 £ x ) Ù ( s = (k+1)2 ) Ù ( n=2k+1 ) Þ ( ( s > x ) Þ
(k2 £ x) Ù ( x < (k+1)2 )
Доказательство истинности условий Ua.
Истинность всех трех условий легко проверяется подстановкой.
4.1. Условие Ua1– истина, так как
выражение( x ³ 0 ) Þ ( ( 02 £ x ) Ù (1 = 1) Ù (1 = 1) ) º
(x ³ 0) Þ (0 £ x) º Ø(x ³ 0) Ú (0 £ x) º (x < 0) Ú (x ³ 0) º true
4.2. Преобразуем условие Ua2.
( k2 £ x ) Ù ( s = (k+1)2 ) Ù ( n=2k+1 ) Þ ( (s £ x) Þ
( (k+1)2 £ x ) Ù ( s + n +2 = (k+2)2 ) Ù ( (n+2) = 2( k+1) +1) ) º
( ( k2 £ x ) Ù ( s = (k+1)2 ) Ù ( n=2k+1 ) Ù (s £ x) ) Þ
( (k+1)2 £ x ) Ù ( s + n +2 = (k+2)2 ) Ù ( (n+2) = 2( k+1) +1) )
Для доказательства истинности условия Ua2 нужно показать, что соотношения, образующие конъюктивные члены справа от знака импликации, следуют из соотношений, стоящих слева от знака импликации.
а) Поскольку x ³ sи s = (k+1)2, то (k+1)2 £ x.
б) s+n+2 = (k+1)2 + 2k + 1 + 2 º k2 + 2k+ 1+ 2k + 1 + 2 = (k+2)2
в) n+2 = 2 (k+1) +2 = 2 (k+1)+1
Следовательно, условие истинно.
4.3. Преобразуем условие Ua3.
( k2 £ x ) Ù ( s = (k+1)2 ) Ù ( n=2k+1 ) Þ ( ( s > x ) Þ
(k2 £ x) Ù ( x < (k+1)2 ) º
( k2 £ x ) Ù ( s = (k+1)2 ) Ù ( n=2k+1 ) Ù ( s > x ) Þ
(k2 £ x) Ù ( x < (k+1)2 )
Поскольку s > xи s = (k+1)2, то (k+1)2 > xи Ua3 – истина