Команда присваивания
Команда присваивания
Присваивание простым переменным
x:=e, где e может быть выражением и e вычислимо.
wp(“x:=e”,R)=domain(e) cand R,
где cand – короткое and.
R- вместо х подставляем е.
Можно записать так: wp(“x:=e”,R)= R.
Примеры:
- wp(“x:=5”,x=5)=(5=5)=T
- wp(“x:=5”,x≠5)=(5≠5)=F
- wp(“x:=x+1”,x<0)=(x+1<0)=(x<-1)
- wp(“x:=x*x”,x4=10)=((x*x)4=10)=(x8=10)
- wp(“x:=a/b”,p(x))=((b≠0)Ùp(a/b))
- wp(“x:=e”,y=c)=(y=c)
- wp("x:=e",y=c)=(y=c)
Рекомендуемые материалы
Выполнение присваивания может изменять лишь ту переменную, которая стоит в его левой части.
Обмен местами значений двух переменных:
wp(“t:=x; x:=y; y:=t”,x=X Ù y=Y) =
wp(“t:=x; x:=y”, wp(“y:=t”, x=X Ù y=Y))=
wp(“t:=x; x:=y”, x=X Ù t=Y)=
wp(“t:=x”,wp(“x:=y”, x=X Ù t=Y))=
wp(“t:=x”, y=X Ù t=Y)=( y=X Ù x=Y)
Кратные присваивания простым переменным
x1,х2,…,хn:=e1,e2,…,en.
Пример: х,у:=у,х – поменять местами значения двух переменных.
Алгоритм присваивания:
- сначала вычисляются все выражения с е1 до еn.
- в результате получаем некие значения v1,v2,…,vn.
- после этого x1 присваиваем значение v1,
x2 присваиваем значение v2,
….
xn присваиваем значение vn.
Пример:
х,х:=1,2
х:=2.
Определяем через wp:
wp(“ ”,R)=domain() cand R.
domain()=("i:domain(ei))
Пример:
1. wp(“x,y:=y,x”,x=X,y=Y)=(x=XÙy=Y)=( y=X Ù x=Y)
2. wp(“z,y:=z*x,y-1”,y≥0 Ù z*xy=c)=((y-1≥0) Ù (z*x*xy-1=c))=
=((y≥1) Ù (z*xy=c))
3. wp(“s,i:=s+b[i],i+1”, i>0 Ù s=: 0≤j<i : b[j])
Поиск решений – утверждений с помощью WP
Даны 3 переменных, между которыми выполняется соотношения i ≤ m < i+p.
Дан массив: b[ i : i+p-1]
Нужно массив сократить так чтобы i:=m+1, но правая граница должна остаться на месте. Нужно найти чему равно Р.
Запишем задачу спецификаций
с – правая граница
{i+p=c} i,p:=m+1,x {i+p=c}
wp(“i,p:=m+1,x”,i+p=c) = (m+1+x=c)
c+p=m+1+x
x=i+p-m-1
тогда i,p:=m+1, i+p-m-1.
Проблемы возникают когда ставятся 2 присваивания.
{T} a:=a+1;b:=x {a=b}
х попадает в зависимость от а.
Решение нужно искать в виде
wp(“a:=a+1; b:=x(a,b)”,a=b) = wp(“a:=a=1”,a=x(a,b))=
=(a+1=x(a+1,b))=(x(a,b)=a)
Присваивание элементу массива
b[i]:=e обозначим b:=(b;i:e) – функциональная запись массива (берем b и по индексу i присваиваем е).
wp(“b[i]:=e”,R)=wp(“b:=(b;i:e)”,R)=domain((b;i:e) cand R=
=domain(“b[i]:=e”,R)=domain(e) cand inrange(b,i) cand R,
i в границах b
Примеры:
- wp(“b[i]:=5”,b[i]=5)=wp(“b=(b;i:5)”,b[i]=5)=((b;i:5)[i]=5) = (5=5)=T
- wp(“b[i]:=5”, b[i]= b[j]) =
((b;i:5)[i]=(b;i:5)[j])=
(((i=j) Ú (5=5)) Ù ((i≠j) Ú (5=b[j])))=
(((i=j) Ù T) Ù ((i≠j) Ú (5=b[j])))=
В лекции "32 Типичные задачи поиска" также много полезной информации.
((i=j) Ú (i≠j) ) Ù ( (i=j) Ú (5=b[j]))=
(T Ù ( (i=j) Ú (5=b[j]) ))=
((i=j) Ú (5=b[j]))
- wp(“b[b[i]]:=i”,b[i]=i)=
((b;b[i]:i)[i]=i)=
(i=b[i]Ùi=i) Ú ( i¹b[i]Ùb[i]=i) = (i=b[i])