Вычисление слабейших предусловий и проверка эквивалентности программ

[marokanin]

Здравствуйте. Попалась мне вот такая лаба, где нужно сделать Вычисление слабейших предусловий и проверку эквивалентности программ.
Первое задание.... мне если честно ни о чём вообще не говорит.

ЗАДАЧА 1:
Дано постусловие программы:

R: ( X = B | || | & A < B + 2 )

и текст программы:

S: Y := A - B + 17;
B := X + Y;
X := A + 25 - B ;
Y := X + 12;
X := X + Y + 7

Вычислить слабейшее предусловие.
я нашёл по ней лишь следующее:
Слабейшее предусловие – предикат wp(S, R), показывающий какие самые слабые условия необходимо наложить на исходные данные, чтобы получить результат исполнения алгоритма удовлетворял R
Тогда условие правильности программы:
Q Þ wp(S, R)
Если Q сильнее wp(S, R) то программа верна

Вторая задача:
ЗАДАЧА 2:
Даны программы:


S1: if α then
else
if β then
E1
else
E2


S2: if ⌐ α then
if ⌐ β then
E2
else
E1

Эквивалентны ли эти программы? Доказать.
Я подумал тут нужно сделать простейшие подставления.. в таком случае программы не эквивалентны. А на самом деле - задание так и осталось непонятным. Пожалуйста помогите, ибо в этом случае моя логика разбилась об это((

[s-andriano]

Сообщение от marokanin

...ибо в этом случае моя логика разбилась об это((

Вообще-то, насколько я понимаю, задание не на логику, а на механическое применение известных правил.

Ну а если эти правила Вам не известны, и Вашей логики не хватает на то, чтобы вывести эти правила самостоятельно, почитайте учебник. Обычно помогает.

[marokanin]

Боюсь не помогает.

[marokanin]

Сообщение от marokanin

Боюсь не помогает.

Проштудировал на эту тему учебное пособие... 0... может всё-таки подскажете что-то конкретное?