Операционная семантика - Operational semantics

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

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

Возможно, первым формальным воплощением операционной семантики было использование лямбда-исчисление определить семантику LISP.^[1] Абстрактные машины в традициях Машина SECD также тесно связаны.

История

Понятие операционной семантики было впервые использовано при определении семантики Алгол 68.Следующее утверждение является цитатой из исправленного отчета ALGOL 68:

Смысл программы на строгом языке объясняется в терминах гипотетического компьютера, который выполняет набор действий, составляющих разработку этой программы. (Алгол68, Раздел 2)

Первое использование термина «операционная семантика» в его нынешнем значении приписываетсяДана Скотт (Плоткин04 Далее следует цитата из основополагающей статьи Скотта по формальной семантике, в которой он упоминает «операционные» аспекты семантики.

Было бы хорошо стремиться к более «абстрактному» и «чистому» подходу к семантике, но для того, чтобы план был хорошим, нельзя полностью игнорировать эксплуатационные аспекты. (Скотт70 )

Подходы

Гордон Плоткин представили структурную операционную семантику, Роберт Хиб и Маттиас Фелляйзен контексты редукции,^[2] и Жиль Кан естественная семантика.

Семантика малого шага

Структурная операционная семантика

Структурная операционная семантика (также называемый структурированная операционная семантика или же семантика малого шага) был представлен Гордон Плоткин в (Плоткин81 ) как логическое средство определения операционной семантики. Основная идея, лежащая в основе SOS, состоит в том, чтобы определить поведение программы с точки зрения поведения ее частей, тем самым обеспечивая структурную, то есть синтаксически ориентированную и индуктивный, взгляд на операционную семантику. Спецификация SOS определяет поведение программы с точки зрения (набора) переходное отношение (s). Спецификации SOS представлены в виде набора правила вывода которые определяют допустимые переходы составного фрагмента синтаксиса с точки зрения переходов его компонентов.

В качестве простого примера мы рассмотрим часть семантики простого языка программирования; надлежащие иллюстрации даны в Плоткин81 и Хеннесси90, и другие учебники. Позволять ${ displaystyle C_ {1}, C_ {2}}$ диапазон программ языка, и пусть ${ displaystyle s}$ диапазон состояний (например, функции от ячеек памяти до значений). Если у нас есть выражения (в диапазоне от ${ displaystyle E}$ ), значения ( ${ displaystyle V}$ ) и локации ( ${ displaystyle L}$ ), то команда обновления памяти будет иметь семантику:

${ displaystyle { frac { langle E, s rangle Rightarrow V} { langle L: = E ,, , s rangle longrightarrow (s uplus (L mapsto V))}}}$

Неформально правило гласит, что "если выражение ${ displaystyle E}$ в состоянии ${ displaystyle s}$ сводится к стоимости ${ displaystyle V}$ , тогда программа ${ displaystyle L: = E}$ обновит состояние ${ displaystyle s}$ с заданием ${ Displaystyle L = V}$ ".

Семантика последовательности может быть задана следующими тремя правилами:

${ displaystyle { frac { langle C_ {1}, s rangle longrightarrow s '} { langle C_ {1}; C_ {2} ,, s rangle longrightarrow langle C_ {2}, s ' rangle}} quad quad { frac { langle C_ {1}, s rangle longrightarrow langle C_ {1}', s ' rangle} { langle C_ {1}; C_ {2} ,, s rangle longrightarrow langle C_ {1} '; C_ {2} ,, s' rangle}} quad quad { frac {} { langle mathbf {skip}, s rangle longrightarrow s}}}$

Неформально первое правило гласит, что если программа ${ displaystyle C_ {1}}$ в состоянии ${ displaystyle s}$ заканчивается в состоянии ${ displaystyle s '}$ , то программа ${ Displaystyle C_ {1}; C_ {2}}$ в состоянии ${ displaystyle s}$ сведется к программе ${ displaystyle C_ {2}}$ в состоянии ${ displaystyle s '}$ . (Вы можете думать об этом как о формализации "Вы можете запустить ${ displaystyle C_ {1}}$ , а затем запустите ${ displaystyle C_ {2}}$ используя полученное хранилище памяти.) Второе правило гласит, что если программа ${ displaystyle C_ {1}}$ в состоянии ${ displaystyle s}$ можно свести к программе ${ displaystyle C_ {1} '}$ с государством ${ displaystyle s '}$ , то программа ${ Displaystyle C_ {1}; C_ {2}}$ в состоянии ${ displaystyle s}$ сведется к программе ${ Displaystyle C_ {1} '; C_ {2}}$ в состоянии ${ displaystyle s '}$ . (Вы можете думать об этом как о формализации принципа для оптимизирующего компилятора: «Вам разрешено преобразовывать ${ displaystyle C_ {1}}$ как если бы она была автономной, даже если это всего лишь первая часть программы. ") Семантика является структурной, потому что смысл последовательной программы ${ Displaystyle C_ {1}; C_ {2}}$ , определяется значением ${ displaystyle C_ {1}}$ и значение ${ displaystyle C_ {2}}$ .

Если у нас также есть логические выражения для состояния с диапазоном ${ displaystyle B}$ , то мы можем определить семантику пока команда: ${ displaystyle { frac { langle B, s rangle Rightarrow mathbf {true}} { langle mathbf {while} B mathbf {do} C, s rangle longrightarrow langle C; mathbf {while} B mathbf {do} C, s rangle}} quad { frac { langle B, s rangle Rightarrow mathbf {false}} { langle mathbf {while} B mathbf {do} C, s rangle longrightarrow s}}}$

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

Благодаря своему интуитивно понятному виду и простой для понимания структуре SOS приобрела большую популярность и стала де-факто стандартом в определении операционной семантики. В знак успеха исходный отчет (так называемый Aarhusreport) о SOS (Плоткин81 ) привлек более 1000 цитирований по данным CiteSeer [1], что делает его одним из самых цитируемых технических отчетов в Информатика.

Семантика редукции

Семантика редукции являются альтернативным представлением операционной семантики с использованием так называемых контекстов редукции. Метод был представлен Робертом Хибом и Маттиас Фелляйзен в 1992 г. как метод оформления эквациональная теория за контроль и государственный. Например, грамматика простого вызов по стоимости лямбда-исчисление и его контексты могут быть заданы как:

${ Displaystyle е = v ; | ; (е ; е) ; | ; x quad quad v = lambda xe quad quad C = left [, right] ; | ; (C ; e) ; | ; (v ; C)}$

Контексты ${ displaystyle C}$ включить отверстие ${ Displaystyle влево [, вправо]}$ где термин может быть вставлен. форма контекстов указывает, где может произойти редукция (т.е. термин может быть вставлен в термин) .Для описания семантики для этого языка предусмотрены аксиомы или правила редукции:

${ displaystyle ( lambda x.e) ; v longrightarrow e , left [x / v right] quad ( mathrm { beta})}$

Эта единственная аксиома является бета-правилом лямбда-исчисления. Контексты редукции показывают, как это правило сочетается с более сложными терминами. В частности, это правило может срабатывать для позиции аргумента приложения, например ${ Displaystyle (( лямбда х.х ; лямбда х.х) лямбда х. (х ; х))}$ потому что есть контекст ${ Displaystyle ([,] ; лямбда х. (х ; х))}$ что соответствует термину. В этом случае контексты однозначно разлагают термины, так что на любом данном шаге возможна только одна редукция. Расширение аксиомы для соответствия контекстам редукции дает совместимое закрытие. Взяв рефлексивное, транзитивное замыкание этого отношения, получаем редукционное отношение для этого языка.

Этот метод полезен для простоты, с которой контексты сокращения могут моделировать состояния или управляющие конструкции (например, продолжения ). Кроме того, семантика редукции использовалась для моделирования объектно-ориентированный языки,^[3] контрактные системы, и другие языковые функции.

Семантика большого шага

Естественная семантика

Структурная операционная семантика большого шага также известна под названиями естественная семантика, реляционная семантика и семантика оценки.^[4] Операционная семантика большого шага была представлена под названием естественная семантика к Жиль Кан представляя Mini-ML, чистый диалект Язык ML.

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

Семантика большого шага описывает способом «разделяй и властвуй», как можно получить окончательные результаты оценки языковых конструкций путем объединения результатов оценки их синтаксических аналогов (подвыражений, подзапросов и т. Д.).

Сравнение

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

Семантика большого шага имеет то преимущество, что часто проще (требует меньшего количества правил вывода) и часто напрямую соответствует эффективной реализации интерпретатора для языка (отсюда Кан назвал их «естественными»). И то, и другое может привести к более простым доказательствам, например при доказательстве сохранения правильности при некоторых преобразование программы.^[5]

Основным недостатком семантики большого шага является то, что без завершения (расходящийся ) вычисления не имеют дерева вывода, что делает невозможным сформулировать и доказать свойства таких вычислений.^[5]

Семантика малых шагов дает больший контроль над деталями и порядком оценки. В случае инструментальной операционной семантики это позволяет операционной семантике отслеживать, а специалисту по семантике формулировать и доказывать более точные теоремы о поведении языка во время выполнения. Эти свойства делают семантику малых шагов более удобной при доказательстве правильность типа системы типов против операционной семантики.^[5]

Смотрите также

внешняя ссылка

СМИ, связанные с Операционная семантика в Wikimedia Commons

[1] Джон Маккарти. "Рекурсивные функции символьных выражений и их машинное вычисление, часть I". Архивировано из оригинал на 2013-10-04. Получено 2006-10-13.

[2] Felleisen, M .; Хиб, Р. (1992). «Пересмотренный отчет по синтаксическим теориям последовательного управления и состояния». Теоретическая информатика. 103 (2): 235–271. Дои:10.1016/0304-3975(92)90014-7.

[3] Abadi, M .; Карделли, Л. (8 сентября 2012 г.). Теория объектов. ISBN 9781441985989.

[4] Университет Иллинойса CS422

[leroy-coinductivebigstep-5] а ^б ^c Ксавье Леруа. «Коиндуктивная операционная семантика большого шага».

[1]

[2]

[3]

[4]

[5]