Соответствие спецификации
Если Р - объект, отвечающий спецификации S, то говорят, что Р удовлетворяет S, сокращенно Р уд S.
Это означает, что S описывает все возможные результаты наблюдения за поведением Р, или, другими словами, S истинно всякий раз, когда его переменные принимают значения, полученные в результате наблюдения за объектом Р, или, более формально:
" пр.пр 
препротоколы (Р) 
S.
В следующих законах приводятся наиболее общие свойства отношения удовлетворяет. Спецификации истина, не накладывающей никаких ограничений на поведение, будут удовлетворять все объекты.
L 1. P уд истина.
Если объект удовлетворяет двум различным спецификациям, он удовлетворяет также и их конъюнкции:
L 2 А. Если Р уд S и Р уд Т, то Р уд (S AND T).
Пусть S (n) — предикат, содержащий переменную n и Р не зависит от n.
L 2 B. Если " n. (Р уд S (n)), то Р уд " n. S (n).
Если из спецификации S логически следует другая спецификация T, то всякое наблюдение, описываемое S, описывается также и Т.
LЗ. Если Р уд S и S T, то Р уд Т.
Доказательства
При проектировании изделия разработчик несёт ответственность за то, чтобы оно соответствовало своей спецификации. Эта ответственность может быть реализована посредством обращения к методам соответствующих разделов математики. В этом разделе мы приводим набор законов, позволяющих с помощью математических рассуждений убедиться в том, что процесс Р соответствует своей спецификации S.
|
|
|
Результатом наблюдения за процессом СТОП всегда будет пустой протокол:
L 4 А. СТОП уд (пр = <>).
Протокол процесса (с 
Р) вначале пуст. Каждый последующий протокол начинается с c, а его хвост является протоколом Р.
L 4 В. Если Р уд S (пр), то (с Р) уд (пр = <> OR (пр 0 = c AND S (пр '))).
Все приведенные выше законы являются частными случаями закона для обобщенного оператора выбора:
L 5. Если " x B. (Р (x) уд S (пр, х)), то
(х: В Р (x)) уд (пр = <> OR (пр 0 B AND S (пр ', пр 0))).
Закон, устанавливающий корректность рекурсивно определенного процесса.
L 6. Если F (X) — предваренная, СТОП уд S, а ((X уд S) (F (Х) уд S)), то
(m Х.F (Х)) уд S.
Пример 1.16. Докажем, что ТАП уд ТАПВЗАИМ.
Доказательство.
1) СТОП уд (пр = <>) 0 
(пр ¯ мон – пр ¯ шок) 1), т.к.
(<> ¯ мон) = (<> ¯ шок) = 0.
Это заключение сделано на основании применения законов L 4 A и L З.
2) Предположим, что Х уд (0 ((пр ¯ мон) – (пр ¯ шок)) 1). Тогда
(мон шок Х) уд (пр < мон, шок > OR (пр ³ < мон, шок >
AND (0 ((пр "¯ мон) – (пр "¯ шок)) 1)))
(0 ((пр ¯ мон) – (пр ¯ шок)) 1),
так как
<> ¯ мон = <> ¯ шок = < мон > ¯ шок = 0, а < мон > ¯ мон =
= < мон, шок > ¯ мон = < мон, шок > ¯ шок = 1 и пр ³ < мон, шок >
((пр ¯ мон = пр " ¯ мон + 1) AND (пр ¯ шок = пр " ¯ шок +1)).
|
|
|
Применяя теперь закон L 3, а затем — L 6, получим требуемый результат.
Тот факт, что процесс Р удовлетворяет спецификации, еще не означает, что он будет нормально функционировать. Например, так как
пр = <> 0 ((пр ¯ мон) – (пр ¯ шок)) 1,
то с помощью законов L 3, L 4 можно доказать, что
СТОП уд 0 ((пр ¯ мон) – (пр ¯ шок)) 1.
Однако СТОП не соответствует ни требованиям владельца торгового автомата, ни покупателя. Он не сделает ничего плохого, но только потому, что он не делает ничего вообще. По той же причине СТОП удовлетворяет любой спецификации, которой может удовлетворять процесс.
Дата добавления: 2015-12-20; просмотров: 21; Мы поможем в написании вашей работы! |
Мы поможем в написании ваших работ!