Логическая семантика языка программирования
Всякая программа содержит логику. Это, например, бизнес-логика, извлекаемая нетривиальным анализом из текста программы в процессе реинжиниринга программы [16]. Это также логические формулы, получаемые по программе в соответствии с формальной семантикой языка программирования (денотационной [8] или аксиоматической [9; 10]) в целях формального доказательства свойств программы.
Проанализируем происхождение логики программы. На рис. 2 представлена общая схема, отражающая связи задачи и программы. Программа является реализацией алгоритма решения некоторой математической задачи. Алгоритм строится с использованием свойств (утверждений, лемм, теорем), доказуемых из условия задачи. Описание алгоритма обычно является содержательным. Программа является результатом кодирования алгоритма на языке программирования.
Рис. 2. Связи между задачей и программой
Логика алгоритма включает свойства, использованные для построения алгоритма. Логика программы является трансформацией логики алгоритма вследствие кодирования алгоритма в конструкциях и структурах данных языка программирования. Оптимизации, совершаемые в процессе кодирования алгоритма в императивной программе, обычно приводят к трансформации логики, усложняя (искривляя) ее.
Формальная семантика языка программирования признана элегантным и мощным формализмом, однако не для реально используемого императивного языка программирования. Для него денотационная семантика оказывается сложной и громоздкой из-за сложности самого языка, а аксиоматическая семантика может быть построена лишь для некоторого простого подмножества языка. Эта оценка, данная Джоном Бэкусом 30 лет назад в своей тьюринговской лекции [17], остается справедливой в настоящее время для современных императивных языков. Таким образом, императивные языки - это языки сложной и кривой логики, которую весьма трудно извлечь из программы.
Логическая семантика является простейшим способом определения логики программы. Логическая семантика есть функция LS, сопоставляющая каждой исполняемой конструкции S соответствующую формулу LS на языке исчисления предикатов, т. е. LS(S) = LS.
Определение логической семантики покажем на примере трех операторов языка исчисления вычислимых предикатов CCP [4] [3]. Подробное описание языка CCP будет дано в следующем разделе. Язык CCP определен как минимальное ядро, из которого можно породить любой чистый язык функционального программирования применением иерархической системы обозначений, свойственных языку. Таким способом определен язык предикатного программирования [7]; его описание будет дано в гл. 6.
Пусть A и B обозначают операторы, x, y и z - различные непересекающиеся наборы переменных. Обозначение A: x ® y определяет оператор A с набором аргументов x и набором результатов y.
Оператор суперпозиции A; B определяет последовательное исполнение операторов A: x ® z и B: z ® y. Логическая семантика оператора суперпозиции определяется следующим образом:
LS(A; B)(x, y) @ $z ( LS(A)(x, z) & LS(B)(z, y) ) . (2.1)
Параллельный оператор A || B определяет параллельное исполнение операторов A: x ® y и B: x ® z. Логическая семантика определяется формулой:
LS(A || B) (x, y, z) @ LS(A)(x, y) & LS(B)(x, z) . (2.2)
Условный оператор if (C) A elseB определяет исполнение одного из операторов A: x ® y и B: x ® y в зависимости от значения логического выражения C, зависящего от x. Логическая семантика определяется формулой
LS(if (C) A elseB) (x, y) @ (C Þ LS(A)(x, y)) & (ØC Þ LS(B)(x, y)) . (2.3)
Правильность построения логической семантики определяется сопоставлением с операционной семантикой языка программирования. Предикат RUN(S, x, y) обозначает следующее утверждение: существует такое исполнение конструкции S для набора значений x, которое завершается, и результатом исполнения является набор значений y. Данное определение допускает неоднозначность при исполнении S: в результате исполнения может быть получен другой набор y’, отличный от y.
Для конструкции S определим свойство согласованности (consistency) Cons(S): предикат LS(S) является истинным на наборах значений x и y тогда и только тогда, когда существует исполнение S для набора x, завершающееся вычислением набора значений y. Формально:
Cons(S) @ "x "y (LS(S)(x, y) Û RUN(S, x, y)) . (2.4)
Логическая семантика согласована с операционной семантикой, если свойство согласованности истинно для всех конструкций языка программирования.
Логическая и операционная семантика языка CCP и доказательство согласованности двух семантик описываются в следующем разделе.
Логическая семантика очевидным образом определяется для языков логического программирования. Однако в этом нет необходимости, поскольку логические формулы, входящие в программу, трактуются в общеизвестном математическом смысле. Построение логической семантики оказывается полезным лишь для нелогических особенностей логического программирования, таких как ситуация «неудачи» при ложном значении в Прологе; описание семантики с учетом данных особенностей дается в четырехзначной логике [14]. Логическая семантика может быть определена для языка предикативного программирования Э. Хехнера [15]. Программа там строится как результат последовательного уточнения (refinement) спецификации программы в виде логической формулы. Уточнения реализуются применением системы правил логического вывода.
Логическая семантика может быть построена для чистых [5] языков функционального программирования. Каждой конструкции языка функционального программирования можно сопоставить эквивалентную формулу на языке исчисления предикатов. Проблематично построение логической семантики для императивных языков. В логической формуле LS для оператора S кроме переменных, явно встречающихся в операторе S, должны участвовать другие переменные, определяющие состояние памяти исполняемой императивной программы.