Правила корректности для условного оператора. Рассмотрим спецификацию условного оператора в виде тройки Хоара:

Рассмотрим спецификацию условного оператора в виде тройки Хоара:

{P(x)} if ( C) A else B {Q(x, y)} [10]. (2.19)

Предположим, что операторы A и B корректны. Их спецификации представлены тройками:

{P_A(x)} A {Q_A(x, y)}, {P_B(x)} B {Q_B(x, y)}.

Определим правила, гарантирующие корректность условного оператора (2.19).

Правило LC1. P(x) & Q(x, y) & C ├ P_A(x) & Q_A(x, y).

Правило LC2. P(x) & Q(x, y) & ØC ├ P_B(x) & Q_B(x, y).

Лемма 2.12. Допустим, спецификация условного оператора (2.19) реализуема, операторы A и B однозначны в области предусловий и корректны, а их спецификации однозначны. Если правила LC1 и LC2 истинны, то условный оператор (2.19) является корректным.

Доказательство. Поскольку операторы A и B однозначны, то и условный оператор (2.19) является однозначным. В соответствии с теоремой 2.1 для доказательства леммы достаточно доказать истинность формулы:

P(x) & Q(x, y) Þ LS(if ( C) A else B)(x, y).

В соответствии с (2.3) формула LS(if ( C) A else B)(x, y) эквивалентна

(C Þ LS(A)(x, y)) & (ØC Þ LS(B)(x, y)).

Пусть истинны P(x) и Q(x, y). Докажем истинность формулы C Þ LS(A)(x, y). Пусть истинно C. Докажем истинность LS(A)(x, y). Можно применить правило LC1, поскольку истинны P(x), Q(x, y) и C. Получим истинность формулы P_A(x) & Q_A(x, y). В соответствии с леммой 2.9 истинна формула

P_A(x) & Q_A(x, y) Þ LS(A)(x, y).

Поскольку истинна посылка, то истинно LS(A)(x, y). Следовательно, доказана истинность формулы C Þ LS(A)(x, y). Истинность формулы ØC Þ LS(B)(x, y) доказывается аналогично. □

Заключение

Корректность программы определяется для класса программ с предикатной спецификацией и для языков с логической семантикой. Представленную модель корректности естественно рассматривать как развитие модели Хоара [9]. Использование свойств логической семантики позволяет определить корректность программы в виде явной логической формулы (2.10), в которой программа S представлена логическим эквивалентом LS(S). В случае, когда оператор S является однозначным, а спецификация реализуема и однозначна, можно использовать формулу корректности (2.16) в соответствии с теоремой тождества спецификации и программы.

Важнейшей особенностью всех правил доказательства корректности является то, что они не используют формул LS(A) и LS(B) - только спецификации (предусловия и постусловия) операторов A и B встречаются в правилах. Это определяет универсальную применимость правил для любых языков программирования, в том числе императивных, для которых проблематично построить логическую семантику - для применимости достаточно того, чтобы программная композиция пары операторов A и B по форме соответствовала одному из указанных трех операторов языка CCP.

Системы правил доказательства корректности определяют алгоритм доказательства корректности программ. Данный алгоритм можно использовать для реализации системы автоматической верификации корректности. Эта система будет существенно более эффективной по сравнению с системой верификации, построенной с использованием формул (2.10) и (2.16). Алгоритм доказательства корректности можно также использовать как метод доказательства «вручную», т. е. в традиционном математическом стиле. Этот метод применялся для доказательства корректности нетривиального алгоритма МакКрейта построения дерева суффиксов [6].

Отсутствие операторов цикла в рассматриваемом наборе операторов не позволяет полноценно показать новую технику доказательства корректности на примерах программ. Аналогами циклов в языке CCP являются рекурсивные определения предикатов. Доказательство корректности рекурсивно определяемых предикатов реализуется с применением структурной и полной индукции [2]; см. гл. 3.

Язык CCP может быть использован в качестве ядра при построении любого чистого языка функционального программирования в виде иерархической системы обозначений. Например, рассмотрим обобщенный оператор суперпозиции A; B для операторов вида A: x®z, r и B: z, x®p, где x, z, r и p обозначают разные наборы переменных, причем наборы x и r могут быть пустыми. Обобщенный оператор A; B может быть определен в виде композиции простого оператора суперпозиции и параллельного оператора. При этом правила доказательства корректности для обобщенного оператора суперпозиции нетрудно получить из соответствующих правил для простого оператора суперпозиции и параллельного оператора.

Список литературы

1. Дейкстра Э. Дисциплина программирования: Пер. с англ. М.: Мир, 1978. 272 с.

2. Шелехов В. И. Модель корректности программ на языке исчисления вычислимых предикатов. Новосибирск, 2007. 51 с. (Препр. / ИСИ СО РАН; № 145).

3. Шелехов В. И. Исчисление вычислимых предикатов. Новосибирск, 2007. 24 с. (Препр. / ИСИ СО РАН; № 143).

4. Шелехов В. И. Анализ общего понятия программы // Методы предикатного программирования. Новосибирск, 2006. Вып. 2. C. 7–16.

5. Шелехов В. И. Язык спецификации процессов // Методы предикатного программирования. Вып.2. Новосибирск, 2006. C. 17–34.

6. Шелехов В. И. Разработка программы построения дерева суффиксов в технологии предикатного программирования. Новосибирск, 2004. 52 с. (Препр. / ИСИ СО РАН; № 115).

7. Шелехов В. И. Введение в предикатное программирование. Новосибирск, 2002. 82 с. (Препр. / ИСИ СО РАН; № 100).

8. Scott D. S. and Strachey C. Towards a mathematical semantics for computer languages // Computers and Automata. 1971. P. 19–46.

9. Hoare C. A. R. An axiomatic basis for computer programming // Communications of the ACM. 1969. Vol. 12 (10). P. 576–585.

10. Floyd R. W. Assigning meanings to programs // Proceedings Symposium in Applied Mathematics, Mathematical Aspects of Computer Science. AMS, 1967. P. 19–32.

11. McCarthy J. A basis for a mathematical theory of computation // Computer Programming and Formal Systems. 1963. P. 33–70.

12. Milner R. A. Calculus of Communicating Systems // Lecture Notes in Computer Science, 1980. Vol. 92.

13. Hoare C. A. R. Communicating Sequential Processes. Prentice-Hall. 1985.

14. Andrews J. H. A logical semantics for depth-first Prolog with ground negation // Theoretical computer science. 1997. Val. 184. P. 105–143.

15. Hehner E. C. R. A Practical Theory of Programming, 2nd edition. 2004; URL: http://www.cs.toronto.edu/~hehner/aPToP/

16. Автоматизированный реинжиниринг программ / Под ред. проф. А. Н. Терехова и А. А. Терехова. СПб.: Изд-во С.-Петерб. ун-та, 2000. 332 с.

17. Backus J. Can programming be liberated from the von Neumann style? A. Functional Style and Its Algebra of Programs // Communications of the ACM. 1978. Vol. 21 (8). P. 613–641.