2) если предикат и while _тест имеют значение истинно,то предикат сохраняет это значение после выполнения do _ части. Для рассмотренного примера выше:
1) u + v = u0 + v0 истинно при входе, потому что u=u0, v=v0;
2) если u + v = u0 + v0 и v ¹0, то u + v = u0 + v0 после одновременного присваивания u,v := u +1, v -1.
Однако, если цикл закончился, инвариант сохраняет значение истинно, хотя
while _тест имеет значение ложно, т.е.
u + v = u0 + v0 L v=0.
Из этого следует, что u= u0+v0 L v=0, и функция программы имеет вид
(u, v ³0 ®u,v := u+v,0).
В общем случае, если q является инвариантом в программе while [q] pdo g od, то
1) p L q ® q ° g ( по определению)
2) Ø p Lq ( при окончании).
Отметим, что условие Ø p Lq определяет комментарий конечного отношения программы типа whilt _ do:
while [q] pdo g od [Ø p Lq].
4.5.2Теорема об инварианте
Для любой циклической программы можно придумать не один инвариант, но не все они достаточно строго характеризуют функцию. Для того чтобы определить инвариант, строго характеризующий функцию, рассмотрим теорему об инварианте.
Теорема об инварианте. Пусть
f = [while pdo g od]
Если X0 Î D (f), X Î D (f) и q(X) = f(X) = f(X0)), то
1) q есть инвариант программы while pdo g od,
2) q характеризует f по окончании цикла, т.е.
Ø p(X) Lq(X) ® X = f(X0)
Доказательство теоремы приведено [1].
Инварианты для циклов do _until ,do _while _do:
f = [do g until p od]; q(X) = (f(X) = f ° g(X0))
f = [do g while p do h od]; q(X) = (f(X) = f ° h ° g(X0))
Теорема об инварианте позволяет выполнять систематический вывод инвариантов.
Пример 1: Определить инвариант для цикла while _do программы:
while x ¹ 0 do x, y := x -1, y +a od
1)Oпределим функцию программы: цикл не зацикливается при
x ³ 0, так как на каждом шаге x уменьшается на единицу, а к переменной y прибавляется переменная a, таким образом, начальное значение y увеличится на x*a.
Следовательно, предполагаемая функция f=( x³0®x, y, a:=0,a*x+y, a)
2) докажем это:
function (x, y,a - целые числа)
f=( x³0®x, y, a:=0,a*x+y, a)
program
while x ¹ 0 do x, y := x -1, y +a od
proof
term
Начальное значение x ³ 0 при каждой итерации уменьшается на 1, так что в итоге while _ тест примет значение ложно
pass
while_test true ( доказать (p ® f)=(p ® f ° g))
|
фрагмент |
условие |
x |
y |
|
x0 ¹ 0 |
x0 ¹ 0 |
x1=x0 |
y1=y0 |
|
x,y := x-1, y+a |
x2 = x1 - 1 |
y2 = y1+a |
|
|
f=(x,y,a:= 0,a*x+y,a |
x2 ³ 0 |
x3 =0 |
y3= a0*x2+y2 |
выводы: а) условие: x0 ¹ 0L x2 ³ 0 = x0 ¹ 0L x1 - 1³ 0
= x0 ¹ 0L x0 - 1³ 0
= x0 ¹ 0L x0 ³ 1
= x0 > 0
б) присваивание: x3 =0 y3 = a0 * x2 + y2
= a0 * (x1 - 1)+y1+ a0
= a0 * (x0 - 1) + y0 + a0
= a0 * x0 + y0
Функция программы:
f=(x > 0®x, y, a:=0,a*x+y, a), которая при значении while _теста истина совпадает с заданной функцией.
pass
while_test false (доказать ( Ø p ® f ) = (Øp ® I))
(x = 0 ®( x ³ 0®x, y, a := 0, a*x+y, a))
= (x = 0 ® x, y, a := 0, a*0+y, a)
= (x = 0 ® x, y, a := x, y, a)
т.е. получили тождественную функцию, что и требовалось доказать
pass
result
pass comp
3) определим инвариант:
|
X |
f(X) |
f(X0) |
|
x |
0 |
0 |
|
y |
a*x+y |
a0*x0+y0 |
|
a |
a |
a0 |
Согласно теореме об инвариантах для построения инварианта необходимо приравнять компоненты, соответствующие f(X) и f(X0):
Уважаемый посетитель!
Чтобы распечатать файл, скачайте его (в формате Word).
Ссылка на скачивание - внизу страницы.