Семантическая теория программ. Семантическая теория программ
 Скачать 172.36 Kb.
|
|
Семантическая теория программ. Операционная и декларативные семантики. Принципы и способы технической реализации моделей процессов и структур. 1. СЕМАНТИЧЕСКАЯ ТЕОРИЯ ПРОГРАММ 1.1. Описание смысла программ Наиболее распространенное определение термина «процесс» – это программа, находящаяся на стадии выполнения. Программы могут создаваться вручную, но для разработки некоторых фрагментов могут использоваться автоматизированные средства. Для написания программ используются определенные полностью или частично формальные методы (чаще – языки программирования). Сведения о синтаксисе и семантике языка программирования необходимы пользователю (программисту) и разработчику транслятора для этого языка. Программист использует эту информацию для разработки программ, разработчик транслятора использует корректные определения для того, чтобы осуществить правильную реализацию языка программирования. Описание семантики языка в большинстве случаев осуществляется приведением нескольких простых примеров и кратким поясняющим текстом. Смысл этого текста чаще всего неоднозначен, так что различные читатели могут понимать его по-разному. Программист может получить ошибочное представление о том, что именно будет делать написанная им программа при выполнении, а разработчик может реализовать какую-либо языковую конструкцию иначе, чем разработчики других реализаций того же языка. Задача определения семантики языка программирования рассматривается теоретиками давно, но до сих пор не найдено удовлетворительного универсального решения. Было разработано множество различных методов формального определения семантики. 1.1.1. Операционная семантика Операционная семантика сводится к описанию смысла программы посредством выполнения ее конструкций на реальной или виртуальной вычислительной машине. Смысл конструкции определяется изменениями, произошедшими в состоянии машины после выполнения данной конструкции (оператора). Допустим, что состояние компьютера – это значения всех его регистров и ячеек памяти, в том числе коды условий и регистры состояний. Если просто записать состояние компьютера, выполнить машинную команду, смысл которой нужно определить, затем записать новое состояние машины, а затем сравнить два полученных состояния, то семантика выполняемой команды станет понятной: она представляется изменением в состоянии машины, вызванным выполнением команды. Описание смысла операторов языков программирования высокого уровня с помощью операционной семантики требует создания реального или виртуального компьютера. Аппаратное обеспечение компьютера является чистым интерпретатором его машинного языка. Интерпретатор любого языка программирования можно разработать с помощью программных инструментов, которые для данного языка становятся виртуальной машиной. Будем считать такой интерпретатор «чистым». Семантику языка программирования высокого уровня можно описать, используя «чистый» интерпретатор данного языка. Однако налицо две проблемы. Во-первых, сложность и индивидуальные особенности аппаратного обеспечения и операционного окружения, используемых для запуска чистого интерпретатора, затрудняют понимание выполняемых действий. Во-вторых, выполненное таким образом семантическое описание будет доступно только для пользователей с абсолютно идентичной конфигурацией вычислительной машины и одинаковой операционной системой. Для борьбы с этими проблемами можно заменить реальную машину неким виртуальным компьютером низкого уровня. Регистры, оперативную память, информацию о состоянии и последовательность выполнения операторов – все это можно смоделировать, написав соответствующие программы. Набор команд такой идеализированной виртуальной машины можно создать так, чтобы семантику каждой отдельной команды было легко понять и описать. Кроме того, семантика значительно упрощается, поскольку понятным становится изменение ее состояния. Использование операционного метода для полного описания семантики языка программирования L требует создания двух компонентов. Во-первых, для преобразования языка L в операторы выбранного языка низкого уровня понадобится транслятор. Во-вторых, для языка низкого уровня понадобится разработать виртуальную машину, состояние которой изменяется с помощью команд, полученных после трансляции операторов языка высокого уровня. Как отмечалось выше, изменения состояния этой виртуальной машины определяют смысл данного оператора. Операционную семантику конструкции while языка Си можно описать в терминах следующих простых команд.
Считается, что человек, читающий подобное описание, сам становится «виртуальной машиной» и предполагается способным правильно «выполнить» команды описания семантики и распознать эффект такого «выполнения» команды. Примерами низкоуровневого языка, который можно применять для операционной семантики, являются элементы следующего списка операторов, соответствующих простым управляющим операторам типичного языка программирования: identifier := variable identifier:= identifier + 1 goto metka if variable relop variable goto metka Здесь relop – один из операторов сравнения из набора {= , !=, >, <, >=, <=}, identifier – идентификатор, a variable – переменная или константа. Перечисленные операторы просты и легки для понимания и реализации. Отчасти обобщим приведенные выше три оператора присваивания, что позволит описать более общие арифметические выражения и операторы присваивания. Например: identfier := variable bin_op variable identifier := un_op variable Здесь bin_op – бинарный оператор, a un_op – унарный оператор. Немного усложнят сделанное обобщение типы данных и необходимость их автоматического преобразования. Чтобы описать семантику, например, указателей, массивов, структур, процедур и функций, понадобится ввести некоторое количество новых достаточно простых команд. Чтобы описать операционную семантику функций, рассмотрим следующую систему равенств: f1(p1, p2, ..., pk) = E1, f2(p1, p2, ..., pk) = E2, . . . . . . . . . . . . . fm(p1, p2, ..., pk) = Em. Здесь в левых частях равенств указаны определяемые функции с формальными параметрами p1, p2, ..., pk. В правых частях указаны выражения, содержащие тела этих функций с аргументами, задаваемых некоторыми выражениями, зависящими от входных параметров p1, p2, ..., pk. Операционная семантика интерпретирует эти равенства как систему подстановок. Под подстановкой Каждое равенство fi(p1, p2, ..., pk) = Ei задает в параметрической форме множество правил подстановок: 1, p2, ..., pk; fi(T1, T2, ..., Tk) → Ei; T1, T2, ..., Tk>. Здесь T1, T2, ... , Tk – это фактические аргументы конкретной функции. Это правило позволяет допустить замену вхождения левой его части в какоелибо выражение на его правую часть. Интерпретация системы равенств для получения значений определяемых функций в рамках операционной семантики производится следующим образом. Предположим, задан набор входных данных d1, d2, ..., dk. Сначала осуществляется подстановка этих данных в левые и правые части равенств. При этом по возможности выполняются предопределенные операции, а также выписываются получаемые в результате этого равенства. На последующих шагах просматриваются правые части получаемых равенств. Если правая часть является каким-либо значением, то оно – значение функции из левой части данного равенства. В противном случае правая часть является выражением, содержащим вхождения каких-либо определяемых функций с наборами аргументов. Если для такого вхождения соответствующая функция с данным набором аргументов имеется в левой части какого-либо из полученных равенств, то либо вместо этого вхождения подставляется вычисленное значение правой части этого равенства, либо изменения вообще не производятся. Если эта функция с заданным набором аргументов не является левой частью никакого из полученных равенств, то формируется новое равенство, которое дописывается к уже имеющемуся набору. Формирование равенства получается из исходного равенства для данной функции, только вместо его параметров подставляются аргументы функции. Описанные шаги выполняются до тех пор, пока все определяемые функции не будут иметь вычисленные значения. Рассмотрим систему равенств, определяющую функцию FIBON(n), которая вычисляет значение числа Фибоначчи по его номеру. FIBON (1) = 1, FIBON (2) = 1 FIBON (n)=FIBON (n–1) + FIBON (n–2). Для вычисления значения FIBON (4) выполняются следующие 4 шага.
Фактически первым и до сих пор самым значительным использованием операционной семантики было описание семантики языка программирования PL/I. Разработанная виртуальная машина и правила трансляции языка PL/I были названы общим именем Vienna Definition Language (VDL) вчестьгорода, вкоторомонибылисозданывлабораторияхкорпорацииIBM. Операционная семантика эффективна лишь до тех пор, пока описание языка остается простым и неформальным. Описание машины и транс- лятора VDL языка PL/I получилось очень сложным, так что практическим целям оно не служит. Проблема операционной семантики заключается в том, что она зависит от алгоритмов, а не от гораздо более строгих математических методов. Так получается, что операторы одного языка программирования описываются с помощью операторов другого языка программирования, только более низкого уравнения. В итоге возможна ситуация, когда даже очень простые программные концепции неявным образом выражаются сами через себя. Методы, описываемые в последующих разделах являются более формальными, поскольку они опираются не на машины, а на математические теории доказательств и рекурсивных функций. | |||||||||||||||||||||||||||||||||||||||||||||