Языки программирования. Практический сравнительный анализ



Языки программирования. Практический сравнительный анализ - стр. 96


Оно довольно очевидно. В сущности именно его мы имели в виду, объясняя саму идею преодоления фрагментов. Зафиксируем некоторый фрагмент Ф и обозначим через L(Ф) некоторое точечное условие для его левого конца, а через R(Ф) - некоторое точечное условие для его правого конца. Через "!==>" обозначим отношение выводимости с помощью наших правил преодоления. Получим

                L(Ф) !==> R(Ф)

(П5)            --------------

                  {L} Ф {R}            .

Замечание. Может показаться, что это правило не совсем естественное и следовало бы ограничиться только правильными языковыми конструктами, а не заниматься любыми фрагментами. Действительно, достаточно применять это правило только для присваиваний, ветвлений, циклов и последовательностей операторов. Но верно оно и в том общем виде, в котором приведено (почему?). При этом недостаточно, чтобы точка привязки утверждения L текстуально предшествовала точке привязки R. Нужна именно выводимость в нашем исчислении (почему?).

Конец замечания.

Итак, мы завершили построение исчисления, фиксирующего дедуктивную семантику языка Дейк.

3.5. Применение дедуктивной семантики

Теперь мы полностью готовы к дальнейшему движению по нашей программе-примеру. Предстоит преодолеть цикл (3-11), исходя из предусловия q(3) и имея целью утверждение q(11). Подчеркнем в очередной раз, как важно понимать цель преодоления конструктов (легко, скажем, преодолеть наш цикл, получив постусловие n >= 1, но нам-то хотелось бы q(11) ! ).

Правило преодоления цикла требует инварианта. Но нам годится не любой инвариант, а только такой, который позволил бы в конечном итоге вывести q(11). Интуитивно ясно, что он должен быть в некотором смысле оптимальным - с одной стороны, выводимым из q(3), а с другой - позволяющим вывести q(11). Обычная эвристика при поисках такого инварианта - постараться полностью выразить в нем основную содержательную идею рассматриваемого цикла.

Замечание. Важно понимать, что разумные циклы преобразуют хотя бы некоторые объекты программы.


Содержание  Назад  Вперед