Теорема о команде выбора
Теорема о команде выбора
If - команда выбора, пусть Q предикат
1. QÞBB
2. QÙBiÞwp(Si,R)
тогда QÞwp(If,R)
Доказательство:
Из 2:
"i: QÙ BiÞwp(Si,R) = "I ØQ Ú ØBi Ú wp(Si,R)=
ØQ Ú "I ØBi Ú wp(Si,R) = Q Þ "i Bi Þ wp(Si,R).
Рекомендуемые материалы
Складываем 1 и 2
(QÞBB) Ù (QÞ"I BiÞ wp(Si,R))=
=(QÞ(BB Ù "i BiÞ wp(Si,R))=(Q Þ wp(If,R)).
Пример – поиск методом половинного деления, нужно найти х в массиве b[0:n-1].
b[k]>j
j:=k
Q: ordered(b[0:n-1])Ù0£i<k<j<nÙxÎb[i:j]
{Q}if b[k]£x ® i:=k b[k]³x ® j:=k fi { xÎb[i:j]}
QÞwp(If,R)
Ещё посмотрите лекцию "Последствия радиационных аварий и катастроф" по этой теме.
1. QÞBB=QÞ(b[k]£x)Ú(b[k]³x)=QÞTºT первая посылка выполняется
2.1 Q Ù (b[k]£x)Þ xÎb[k:j]
wp(“i:=k”, xÎb[i:j])
2.2 Q Ù (b[k]³x)Þ xÎb[i:k]
wp(“j:=k”, xÎb[i:j])
Q может использоваться в качестве предусловия.