Частичная и полная коррекция
Частичная и полная коррекция
{Q} S {R} – полная коррекция.
Q { S } R – частичная коррекция.
В частичной коррекции не используется выражение “через конечное время”.
Если выполнение команды S начинается в состоянии, удовлетворяющем Q, и если оно заканчивается, то конечное состояние будет удовлетворять R.
Пример:
T {while T do skip} T – в формате частичной корректности.
Представляет собой бесконечный цикл, который ничего не делает.
Рекомендуемые материалы
{T} while T do skip {T} – данное высказывание тождественно ложно.
Некоторые свойства WP
- Закон исключенного чуда:
wp(S,F)=F
Никакое состояние не может удовлетворять F, т.к. F представляет собой пустое множество.
Пример: wp(a:=a+b,a>a) = False
- Закон монотонности:
Если Q®R, то wp(S,Q)® wp(S,R).
Если R слабее Q, то wp(S,R) слабее wp(S,Q).
Пример: a>0 => a³0 wp(a:=a+1,a>0) => wp(a:=a+1,a³0)
a>-1 => a³-1
- Дистрибутивность конъюнкции:
wp(S,Q)Ù wp(S,R)= wp(S,QÙR)
Пример: wp(a:=a+1,a>0) Ù wp(a:=a+b,b>0) (Левая часть)
a+b>0 b>0
wp(a:=a+b,a>0 Ù b>0) = a+b>0 Ù a>0) (Правая часть)
- Дистрибутивность дизъюнкции:
В лекции "8 Анализ запаздывания" также много полезной информации.
wp(S,Q)Ú wp(S,R) ® wp(S,QÚR)
Действует только в одну сторону.
Пример: Q – выпадение орла, R – выпадение решки, S - бросание монетки.
wp(бросание, орел)Ú wp(бросание, решка)=Т
wp(бросание, решкаÚорел)=Т
Для детерминированных случаев закон действует в обе стороны.