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




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


Язык Дейк удовлетворяет этому принципу.

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

(1)  x := M[1] ;  (2)  i := 1 ;    (3)

     'do' i < n -->   (4)  i := i + 1 ;  (5)

                  'if' M[i] > x -->  (6)  x := M[i] ;  (7)

                       M[i] <= x --> (8)  'null' (9) 'fi' ;  (10)

          'od' ;  (11)

Весь этот фрагмент теперь можно обозначить как Ф(1-11) или даже . просто (1-11). Условие на состояние программы в точке t обозначим через q(t). Так что предусловие для Ф(1-11) получит обозначение q(1), а постусловие q(11). Для обозначения тождества условий будем применять двойное двоеточие. Так что, скажем

                  q(11) :: { x = max(M,n) }       .    

Наконец, в четвертых (самое важное), для каждого языкового конструкта нужно сформулировать правила вывода соответствующих троек Хоара. Эти правила естественно называть дедуктивной семантикой конструкта, а их совокупность для всего языка - дедуктивной семантикой языка. Вскоре мы построим такую семантику для языка Дейк, а пока - несколько предварительных замечаний.              

Как уже сказано, для каждого конструкта языка Дейк нужно сформулировать правило вывода допустимых троек Хоара. Тройки Хоара абсолютны в том смысле, что их истинность не зависит от контекста фрагмента, входящего в тройку (почему?). Однако выводить тройки Хоара удобно с помощью условий, характеризующих состояния программы в отдельных точках. Такие "точечные" условия обычно относительны в том смысле, что их истинность (и выводимость) зависят от других точечных условий.

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


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