Основы объектно-ориентированного проектирования


О правилах доказательств


Этот параграф предназначен для читателей, склонных к математике, остальные могут сразу перейти к обсуждению в следующем разделе. Хотя основные идеи можно понять и без формального освоения теории языков программирования, полное понимание требует знакомства хотя бы с основами этой теории, изложенными, например, в книге [М 1990], обозначения которой здесь будут использоваться.

Основное математическое свойство последовательного ОО-вычисления было полуформально приведено при обсуждении Проектирования по Контракту:

{INV and pre} body {INV and post}

где pre, post и body - это предусловие, постусловие и тело программы, а INV - это инвариант класса. При подходящей аксиоматизации исходных инструкций оно может послужить основой полной формальной аксиоматической семантики ОО-ПО.

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

t.f (..., a, ...)

вызывающие компонент f, возможно, с аргументами такими, как a, для цели t, присоединенной к объекту. Правило доказательства для последовательного случая можно содержательно сформулировать так:

Основной последовательный метод доказательства

Если можно доказать, что тело f, запущенное в состоянии, удовлетворяющем предусловию f, завершит работу в состоянии, удовлетворяющем постусловию, то для указанного выше вызова можно вывести то же свойство, в котором формальные аргументы заменены фактическими. Каждый неквалифицированный вызов в утверждениях вида some_boolean_property заменяется соответствующим свойством t вида t.some_boolean_property.

Например, если мы можем доказать, что конкретная реализация put в классе BOUNDED_QUEUE, запускаемая при выполнении условия not full, выдает состояние, удовлетворяющее not empty, то для любой очереди q и любого элемента a приведенное правило позволяет вывести:

{not q.full} q.put (a) {not q.empty}

Более формально основное правило доказательства можно выразить, приспособив к ОО-вычислениям известное правило Хоара (Hoare) для доказательства вызовов процедур:




Начало  Назад  Вперед



Книжный магазин