Преобразователь предикатов WP
Преобразователь предикатов WP (wp(S,R))
Преобразователь предикатов wp определяет множество всех состояний, для которых выполнение команды S, начавшейся в таком состоянии, закончится через конечное время, в состоянии, удовлетворяющем R.
Пример:
1. wp(“i:=i+1”,i³1)=(i³0)
{i³0}i:=i+1{i³1}
2. S=”if x³y then z:=x else z:=y”
R: z=max(x,y)
wp(S,R)=T
3. S=”if x³y then z:=x else z:=y”
Рекомендуемые материалы
R: z=y
wp(S,R)=(x£y)
4. S=”if x³y then z:=x else z:=y”
R: z=y-1 (этого быть не может)
wp(S,R)=F – предусловием является пустое множество состояний. Никакие значения переменных не сделают z меньше у.
5. S=”if x³y then z:=x else z:=y”
R: z=y+1
wp(S,R)=(х=у+1)
Тема 3. СТРУКТУРА И ЭЛЕМЕНТЫ «ЧЕЛОВЕК И СРЕДА ОБИТАНИЯ» - лекция, которая пользуется популярностью у тех, кто читал эту лекцию.
wp(S,R) (weakest precondition) – слабейшее предусловие в контексте S по отношению к R, поскольку оно определяет множество всех состояний таких, что выполнение, начавшееся в любом из них, закончится при истинном R.
Пример:
Условие а>0 сильнее, чем условие а³0.
Если зафиксируем S, то получим wps(R), т.е. из одного предиката получаем другой.