Соответствие спецификации

Если Р - объект, отвечающий спецификацииS, то говорят, что Р удовлетворяет S, сокращенно Р уд S.

Это означает, что S описывает все возможные результаты наблюдения за поведением Р, или, другими словами, S истинно всякий раз, когда его переменные принимают значения, полученные в результате наблюдения за объектом Р, или, более формально:

"пр.пр препротоколы(Р) S.

В следующих законах приводятся наиболее общие свойства отношения удовлетворяет. Спецификации истина, не накладывающей никаких ограничений на поведение, будут удовлетворять все объекты.

L1.P уд истина.

Если объект удовлетворяет двум различным спецификациям, он удовлетворяет также и их конъюнкции:

L2А.Если Р уд S и Р уд Т, то Р уд (S AND T).

Пусть S(n) — предикат, содержащий переменную n и Р не зависит от n.

L2B.Если "n.(Р уд S(n)), то Р уд "n.S(n).

Если из спецификации S логически следует другая спецификация T, то всякое наблюдение, описываемое S, описывается также и Т.

LЗ.Если Р уд S и S T, то Р уд Т.