Правило вывода для условного оператора if В then А1 else А2 {P B} A1 {Q}, {P } А2 {Q} |-{P} if B then A1 else A2 {Q} (6) Задача Докажем истинность {t} if а>0 then m:=a else m:=-а {m0} По правилу 6: {t a>0} m:=a {m0} и {t } m:=-а {m0} По аксиоме (3): {а 0} m:=а {m0}3 t a>0 a0, {a0} m:=a {m0} |- {t а>0} m:=а {m0} По закону консенквенции: t a>0 а 0 Аксиома для оператора присваивания вида х:= е {Q(x e)}x:=e {Q} (3)
Пример t a 0, {a 0} m:=-a {m0} |- {t } m:=-а {m0} По закону (2) :2 t a 0 а 0 По аксиоме (3): {а 0} m:=-а {m0}3
Схемы циклов и разветвления Р - + A B Р В Р ¬В Р A Q Q B - + B Р - + A1A1 B Р В Q Р ¬В A2A2 а) цикл с предусловиемб) цикл с постусловием в) ветвление