Конечно же, при спецификации больших и сложных программ таким способом могут возникнуть трудности, и чтобы справится с ними можно использовать менее формальные, словесные утверждения дано и получить. Вместе с тем понятно, что можно рассматривать утверждения не только о начальных и конечных состояниях программы, но и утверждения, связанные с произвольной точкой программы и описывающие те состояния ВМ, которые содержат данную точку программы. Например, для ВМ с двумя переменными X и Y два состояния {(X,2),(Y,3)} и {(X,2),(Y,4)} описывает следующее утверждение о значениях переменных X и Y:
(X=2)&((Y=3)or(Y=4)).
Утверждение вообще и логическое выражение в частности выражает, или описывает, множество состояний, в котором оно истинно. Так, пустое множество, не содержащее состояний вообще, представимо логическим выражением false, поскольку false не истинно ни в одном состоянии. Множество всех состояний представимо логическим выражением true, поскольку true истинно во всех состояниях.
Говорят, что утверждение 
слабее
(а утверждение
сильнее, чем утверждение),
если
является следствием
(т.е. истинна импликация 
).
Более сильное высказывание сильнее ограничивает комбинации значений переменных,
описываемых им, а более слабое -- слабее. В терминах множеств состояний
слабее, чем ,
если оно "менее ограничительно": множество состояний, описанное ,
содержит по меньшей мере те состояния, которые описывает ,
а возможно, еще и другие. Слабейшее утверждение -- это true (или
любая другая тавтология): оно представляет множество всех состояний; сильнейшее
утверждение -- это false: оно представляет пустое множество.
Next:2.3.4
Метод промежуточных утверждений Up:2.3
Доказательство свойств программ
Previous:2.3.2
Внешняя спецификация программы