Построение инварианта
Построение инварианта
{Q} do B ® S od {R}
 |
Начиная с R наращиваем до Q.
Ослабление предикатов (точнее предиката R):
1. Устранение конъюнктивного члена
A Ù B Ù C ® A Ù C
Рекомендуемые материалы
n³0
R: 0£a2£n<(a+1)2
0£a£
<(a+1)
R: 0£a2 Ù a2£n Ù n<(a+1)2
P: 0£a2 Ù a2£n
P Ù ØBÞR
B = n³(a+1)2
t: n-a
a:=0
do
n³(a+1)2 ® a:=a+1
do
wp(“a:=a+1”,P) = 0£(a+1)2 Ù (a+1)2£n
PÙn ³ (a+1)2 Þ 0£(a+1)2 Ù (a+1)2
2. Замена константы переменной
Нужно найти суммы элементов массива
b[0:n-1] n>0
R: S=
j: 0£j<n
: b[j] константу n заменяем на i.
P: S=j: 0£j<i: b[j]Ù 0£i£n
Инициализация переменных, чтобы Р было истинно перед циклом
i, S :=0, 0
ограничивающая функция t: n-i
i¹n
do
i¹n ® i,S := i+1, S+b[i]
od
3. Расширение области значения переменной.
Найдем значение вхождения Х в массив b.
b[0:n-1] n>0
iv – const – наименьшее i, удовлетворяющее условию 0£i Ù x=b[i]
R: i=iv
P: 0£i£iv
i:=0;
do
x¹b[i] ® i:=I+1
od
4. Комбинирование предусловия и постусловия
Q: "i: 0£i<n : b[i]=B[i]
R: "i: 0£i<n : b[i]=B[i]+P*i
R вместо ? не подойдет т.к. n-константа
Бесплатная лекция: "9. Селекционная инвентаризация" также доступна.
Р: 0£j£n Ù ("i: 0£i<j : b[i]=B[i]+P*i) Ù ( "i: j£j<n : b[i]=B[i])
Цикл:
j:=0
do
j¹n ® j, b[j] := j+1, b[j]+P*j
od
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
