Наука программирования Дэвида Гриса

"Наука программирования" Дэвида Гриса

Суд по всему, автор книги данной книги, «Наука программирования» существенно расширил формализм алгебры логики (и саму алгебру логики) с целью доказательства алгоритмов. (часть 2)
А также создал новый, более удобный псевдокод для описания алгоритмов с той же целью.
Краеугольным камнем этой методологии являются понятия предусловия и постусловия данного алгоритма (а также каждого его шага, ибо каждый шаг – это тоже алгоритм, только из 1-го действия), что я в своих записях называл просто: начальная и конечная ситуация исполнения алгоритма.

Но при чтении данной книги у вдумчивого читателя возникают вопросы:
1)Что такое состояние? (с.21)
Я понимаю под состоянием состояние данной переменной (после выполнения некоторого шага алгоритма), отличающегося от возможного её другого состояния её значением.
(потому что на самом деле значение всякой переменной при выполнении алгоритма может зависеть не только от наименования данной переменной, но и от последнего выполненного шага алгоритма. Что понятно только программистам, но не математикам, по крайней мере, не всем.)
Грис же понимает под состоянием некую ситуацию в процессе выполнения алгоритма, определяемую как множество значений переменных алгорима. Но у Гриса почему-то все переменные, к которым применется понятие состояние, понимаются как логические переменные.
Ну как же, ведь Грис работает с предикатами, а это логические функции. Но, тем не менее, в алгоритме могут встречаться и переменные других типов. Но Грису не интересны значения всех переменных, т.к. его  понятие "состояние" - это состояние предикатов относительно значений входящих в них переменных (любых типов)

2)Далее, если определено понятие состояние", то непонятно, что такое начальное (и конечное) значение переменной? (с.108) На самом деле это вспомогательные , более частные по отношению к понятию "состояние" понятия, а именно состояние перед выполнеием некоторой операции и после её выполнения. А точнее, значения переменны-аргументов действия-процедуры.

3)Картинки массивов (с.100) - что это? Впрочем, думаю, это не так и актуально, это уже изыски, для практики особого значения не имеет. Если нужно будет, вернёмся к этому.

4)Предикат wp (слабейшее предусловие, то есть условие, дающее самое большое множество допустимых значений исходных переменных для выполнимости данного действия (или алгоритма) за конечное время (то есть он не зацикливается), главное детище Дэвида Гриса) вычисляют по действию S и постусловию R. (с.113)

Легко доказать, что wp от алгоритма (в простейшем случае из 2-х действий):
wp("S1,S2",R)=wp(S1,wp(S2,R))

Но Дэвид Грис выводит следующие архисложные теоремы:
wp("x:=e", R)=domain(e cand R(x,e))(с.113)
Что же это за операция cand?
А вот:
a cand b=if a then b else F
Насколько актуальна данная логическая операция? Чтобы понять это, до кучи напишем определение родственной операции:
a cor b=if a then T else b (с.76),
где
F - тождественная ложь,
T - тождественная истина.
После этого вам понятна степень актуальности данных определений? Лично по мне, она близка к 0.
К тому же чем отличается таблица истинности cand от таблицы истинности and? Ничем.
Ровно то же можно сказать и про операцию cor. Так зачем же было "изобретать велосипед", мистер Грис?

Но мы не выяснили еще, что же такое domain.
По Грису это так:
domain(e) - предикат, описывающий, в которых е определено (с.121)
Касаемо же обозначения R(x,e), так оно определяется так:
предикат, получающийся из предиката R а результате всех свободных вхождений х в R на е. (с.87)
А свободные вхождения переменной x в предикат R - это такие, в которых х не охвачен кванторами. (это уже общепринятое понятие)
Фууу!

Понятно, что:
1)выполнимость действия зависит не только от значений его (входящих) аргументов, но и от их типов
2)у каждого действия есть еще и область значений, которая переходит в область определения следующего действия.
(Но действие - это функция или процедура?
Действие – это не то и не другое.
Ибо действие – это действие, то есть (собственно) операция, то есть сложение, умножение и т.п.
Функция же – это результат применения действия к входным аргументам. (у функции есть только такие)
Процедура же – это сохранение результатов действий в выходных аргументах.)

Но нельзя ли было представить всё это намного проще? Ведь речь-то идёт о самой простой операции, присваивании.
И вообще, странно в этих рассуждениях следующее: зачем заставлять алгоритм давать некоторый желаемый результат? (то есть задавать постусловие)
Ну, я понимаю, предусловие - это аналог области определения совершаемого действия. Например, так:
{b=/=0}a/b{null},
где null - это отсутствие каких-либо требований к результату, то есть тождественная истина: что получится, то и получится. Но получится (что-нибудь, кроме ничего) при условии, что выполняется предусловие: b=/=0)

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

Ведь желаемое для алгоритма – это предикативное описание результата выполнения алгоритма.
Например, требуется выполнить сложение матриц A и B, результат записать в C.
Тогда постусловие таково: R={C=A+B} , и оно, как видим, зависит от собственно алгоритма.
А предусловие (слабейшее, конечно, потому что нет некоторого (неизвестно откуда взявшегося) дополнительного постусловия, после собственно описания требуемого результата алгоритма) таково:
Q={v(n(A)=n(B)=n(С))=T (количество строк матриц)
and
v(m(A)=m(B)=n(C))=T} (количество столбцов матриц)
(при этом требования для n(С) нужно только для статических массивов)
(А лучше не T (т.к это заведомая истина (или тождество или тавтология, что есть синонимы), а t, то есть просто значение логического выражения, true)

Для операции же, описываемой постусловием R={C=A*B} предусловие таково:
Q={(m(A)=n(B)) and (n(C)=n(A)=m(B))}
(При этом требования для n(С) нужно только для статических массивов)

Касаемо же R={a:=b}, то соответственно Q={type(a)=type(b)}, и то не для всех трансляторов, а только для тех, которые не умеют (автоматически) выполнять конвертацию типов или в которых конвертация данных типов (в данные) не определена.)

Таким образом, как постусловие, так и предусловие зависят от производимого нами действия.
Зачем же тогда такие супертонкости, которые вводит Дэвид Грис?