Теория вычислительных процессов (стр. 15 )

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

Семантику конструкции for языка С можно описать в терминах следующих простых команд.

Оператор языка С	Операционная семантика
for (expr1;expr2;eхрrЗ) { }	exrp1 loop:if expr2=0 goto out expr3; goto loop out:

Формальное описание операционной семантики можно представить в виде системы равенств:

,

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

Операционная семантика интерпретирует эти равенства как систему подстановок. Под подстановкой терма в выражение вместо символа будем понимать переписывание выражения с заменой каждого вхождения в него символа на выражение . Каждое равенство задает в параметрической форме множество правил подстановок:

где ‑ конкретные аргументы данной функции. Это правило допускает замену вхождения левой его части в какое-либо выражение на его правую часть.

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

Пример. Рассмотрим систему равенств, определяющую функцию

Для вычисления значения осуществляются 6 шагов.

шаг 1	шаг 2	шаг 3
шаг 4	шаг 5	шаг 6

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

2.3 Аксиоматическая семантика

Аксиоматическая семантика была создана в процессе разработки метода доказательства правильности программ. Семантику каждой синтаксической конструкции языка можно определить как некий набор аксиом или правил вывода, который можно использовать для вывода результатов выполнения этой конструкции. Чтобы понять смысл всей программы, эти аксиомы и правила вывода следует использовать так же, как при доказательстве обычных математических теорем. В предположении, что значения входных переменных удовлетворяют некоторым ограничениям, аксиомы и правила вывода могут быть использованы для получения ограничений на значения других переменных после выполнения каждого оператора программы. Когда программа выполнена, получаем доказательство того, что вычисленные результаты удовлетворяют необходимым ограничениям на их значения относительно входных значений. То есть, доказано, что выходные данные представляют значения соответствующей функции, вычисленной по значениям входных данных.

Такие доказательства показывают, что программа выполняет вычисления, описанные ее спецификацией. В доказательстве каждый оператор программы сопровождается предшествующим и последующим логическими выражениями, устанавливающими ограничения на переменные в программе. Эти выражения используются для определения смысла оператора вместо полного описания состояния абстрактной машины.

Аксиоматическая семантика основана на математической логике. Будем называть предикат, помещенный в программу утверждением. Утверждение, непосредственно предшествующее оператору программы, описывает ограничения, наложенные на переменные в данном месте программы. Утверждение, следующее непосредственно за оператором программы, описывает новые ограничения на те же (а возможно, и другие) переменные после выполнения оператора.

Введем обозначение (триада Хоара)

где ‑ предикаты, ‑ программа (оператор или последовательность операторов). Обозначение определяет следующий смысл: «Если выполнение началось в состоянии, удовлетворяющем , то имеется гарантия, что оно завершится через конечное время в состоянии, удовлетворяющем ».

Предикат называется предусловием или входным утверждением , предикат ‑ постусловием или выходным утверждением, определяет то, что нужно установить ( определяет спецификацию задачи). В предусловии нужно отражать тот факт, что входные переменные получили начальные значения.

Пример. Рассмотрим оператор присваивания для целочисленных переменных и постусловие:

sum:=2*х+1 {sum>1}

Одним из возможных предусловий данного оператора может быть {х>10}.

Слабейшими предусловиями называются наименьшие предусловия, обеспечивающие выполнение соответствующего постусловия. Например, для приведенного выше оператора и его постусловия предусловия {х>10}, {х>50} и {х>1000} являются правильными. Слабейшим из всех предусловий в данном случае будет {х>0}.