примеры решения предикат

где Q1 и Q2 - пока неизвестные предикаты.

Предположим, что цикл заканчивается, тогда первый шаг вывода очевиден:

Решение. Введем следующие обозначения:

r:=x;q:=0;while ry do r:=r-y;q:=q+1 od{r0&r<y&x=qЧy+r}

частное q и остаток r от деления x на y:

Пример 1. Докажем частичную правильность следующей программы, вычисляющей

Примеры решений некоторых упражнений

Упражнение 1. Примеры решений некоторых упражнений