Программа как математический объект: Методические указания для самостоятельного изучения темы и выполнения РГР, страница 18

4) sub = [ m; s; free y]                                 sub Ì [ m; s; free y]

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

4.3. Правильность элементарных программ

4.3.1. Окончание выполнения программы

Если программа является программой без циклов, то она всегда заканчивается и вычисляет какую-либо функцию. Сложнее обстоит дело с циклическими программами, так как для того, что бы исследовать вопрос правильности программы необходимо знать, что она заканчивается.  При этом проблема окончания программы является алгоритмически не разрешимой проблемой. Поэтому мы ограничим пределы нашего рассмотрения программами, окончания которых можно доказать. Определим новый предикат: term(f, P) = « P заканчивается для каждого исходного состояния X Î D (f) ».

4.3.2 Лемма о сведении итерационных  программ к рекурсивным

Даны функции f, g, h и предикат р:

Случай  а)  (while _ do):

 (f=[while p do g od])«(term(f, while p do g od) L f = [if p then g; f fi ])

Случай  b)  ( do _ until):

(f=[ do g until p od])«(term(f, do g until p od) L f = [ g; if  Ø p then f fi ])

 Случай  c)  (do _while _ do):

(f=[do g while p do h od])«(term(f, do g while p do h od) Lf =[g; if p then h; f fi ])

Доказательство леммы см.  [12 ]

На основе этой леммы верификация элементарных циклических программ сводится к верификации ациклических программ типа if _ then. Согласно лемме, программы P = while p do g od и  Q = if p theng; f fi функционально эквивалентны [P] = [Q]. Аналогичные утверждения можно сформулировать относительно двух других случаях.

Пример: рассмотрим программу P, которая складывает два неотрицательных числа u и v:

P = while v > 0 do u, v := u + 1, v - 1 od

Можно заметить, что P завершается и имеет программную функцию

f = (v > 0 ® u, v := u + v,  0 | истина  ® u, v := u , v )

P функционально эквивалентна программе

Q = if v >0 thenu, v := u + 1, v - 1; u, v := u + v,  0 fi

Рассмотрим два случая:  случай Ø (v>0):

Ø (v > 0) и (v > 0)  ® ( v = 0). Программа P в данной точке определена и ровна (u, v:= u,  v). Аналогичный результат  имеет функция  программы Q.

случай (v>0): функция [Q] представляет собой композицию двух функций и может быть определена непосредственной подстановкой, а именно:

[u, v := u + 1, v - 1; u,  v := u + v, 0] = u, v := (u + 1 ) + (v - 1), 0 = u, v := u  + v, 0

Тогда [Q] = (u, v := u  + v, 0 ) = [P], что и требовалось доказать.

4.3.3.  Теорема правильности

Теорема правильности показывает, что все структурированные программы, выраженные через элементарные, содержащие не более одного предиката, могут быть верифицированы ( за исключением вопроса окончания программ) методами, применяемыми при доказательстве правильности программ типа последовательность и if _ then _ else. Проблемы доказательства правильности  могут оказаться слишком трудоёмкими, но теоретически разрешимыми.

Теорема правильности. Для любой функции f и программы P правильность определяется условием С:

1) полная правильность

(f=[P])«(term(f, P) L f={(X, Y) | C(X, Y)})

2) достаточная правильность

(f=[P])«(term(f, P) L f  Ì{(X, Y) | C(X, Y)})