Доказательства

При проектировании изделия разработчик несёт ответственность за то, чтобы оно соответствовало своей спецификации. Эта ответственность может быть реализована посредством обращения к методам соответствующих разделов математики. В этом разделе мы приводим набор законов, позволяющих с помощью математических рассуждений убедиться в том, что процесс Р соответствует своей спецификации S.

Результатом наблюдения за процессом СТОП всегда будет пустой протокол:

L4А.СТОП уд (пр = <>).

Протокол процесса (с Р) вначале пуст. Каждый последующий протокол начинается с c, а его хвост является протоколом Р.

L4В.Если Р уд S(пр), то (с Р) уд (пр = <> OR (пр₀ = c ANDS(пр'))).

Все приведенные выше законы являются частными случаями закона для обобщенного оператора выбора:

L5.Если "x B.(Р(x) уд S(пр, х)), то

(х: В Р(x)) уд (пр = <> OR (пр₀ B AND S(пр', пр₀))).

Закон, устанавливающий корректность рекурсивно определенного процесса.

L6.Если F(X) — предваренная, СТОП уд S, а ((X уд S) (F(Х) уд S)), то

(mХ.F(Х)) уд S.

Пример 1.16. Докажем, что ТАП уд ТАПВЗАИМ.

Доказательство.

1) СТОП уд(пр = <>) 0 (пр ¯ мон – пр ¯ шок) 1), т.к.

(<> ¯ мон) = (<> ¯ шок) = 0.

Это заключение сделано на основании применения законов L4A и LЗ.

2) Предположим, что Х уд (0 ((пр ¯ мон) – (пр ¯ шок)) 1). Тогда

(мон шок Х) уд (пр <мон, шок> OR (пр ³ <мон, шок>

AND (0 ((пр"¯ мон) – (пр"¯ шок)) 1)))

(0 ((пр ¯ мон) – (пр ¯ шок)) 1),

так как

<> ¯ мон = <> ¯ шок = <мон> ¯ шок = 0, а <мон> ¯ мон =

= <мон, шок> ¯ мон = <мон, шок> ¯ шок = 1 и пр ³ <мон ,шок>

((пр ¯ мон = пр" ¯ мон + 1) AND (пр ¯ шок = пр" ¯ шок+1)).

Применяя теперь закон L3, а затем — L6, получим требуемый результат.

Тот факт, что процесс Р удовлетворяет спецификации, еще не означает, что он будет нормально функционировать. Например, так как

пр = <> 0 ((пр ¯ мон) – (пр ¯ шок)) 1,

то с помощью законов L3, L4 можно доказать, что

СТОП уд0 ((пр ¯ мон) – (пр ¯ шок)) 1.

Однако СТОП не соответствует ни требованиям владельца торгового автомата, ни покупателя. Он не сделает ничего плохого, но только потому, что он не делает ничего вообще. По той же причине СТОП удовлетворяет любой спецификации, которой может удовлетворять процесс.