Теорема о цикле и его инварианте
2020-06-032021-03-09zzyxelСтудИзба
Теорема о цикле, его инварианте и ограничивающей функции
Посылки:
1. PÙBi Þ wp(Si,P) - сохранение инварианта
Т.е. если выполняется инвариант и нас пустила i-ая охрана, то выполнение i-ой команды составит истинность P.
Люди также интересуются этой лекцией: Вопрос 19.
2. PÙBB Þ t>0 (т.е. есть еще шаги)
Т.е. если выполняется инвариант и BB, то ограничивающая функция положительна.
3. С каждым шагом ограничивающая функция уменьшается.
PÙBi Þ wp(“t1:=t;SB”,t<t1)
Т.е. если нас пустила i-ая охрана, то выполнение i-ой команды уменьшит функцию.
Вывод: если эти посылки выполняются, то Р можно использовать в качестве предусловия для цикла. P Þ wp( DO ,P Ù ØBB);