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




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


Обычно предполагается, что эта связь тщательно проверена. Впрочем, польза от доказательства не столько в гарантии правильности (в общем случае, конечно, не обеспечиваемой; почему?), сколько в систематическом исследовании программы с нетривиальной точки зрения. Такое исследование, безусловно, способствует нахождению в программе ошибок.

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

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

3.4.1. Дедуктивная семантика присваивания

Начнем, например, преодолевать Ф(1-2), т.е. по q(1) попытаемся построить разумное q(2). Каждый легко напишет

                   

                    q(2) :: ( n >= 1 & x = M[1] )

Но это написано для конкретного предусловия и конкретного оператора присваивания. Как же обобщить и формализовать прием преодоления присваивания, примененный нами только что интуитивно?

Ясно, что мы учли результат выполнения конкретного оператора присваивания Ф(1-2) над конкретными объектами программы x и M[1]. Другими словами, учли операционную семантику присваивания. Результат выполнения состоит в том, что  знак x после выполнения оператора присваивания начинает обозначать то же самое, что до его выполнения обозначал знак M[1]. Другими словами, денотат знака M[1] становится денотатом знака x. Итак, если нам до выполнения присваивания что-то известно про денотат знака M[1], то после выполнения присваивания то же самое можно утверждать и про денотат знака x. Это и есть основная идея описания дедуктивной

семантики оператора присваивания:

всякое утверждение про значение выражения e в операторе вида

                         v := e 

остается верным после выполнения этого оператора по отношению к




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