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

редактировать

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

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

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

Содержание

1 История
2 Подходы
- 2.1 Семантика малых шагов
  - 2.1.1 Структурная операционная семантика
  - 2.1.2 Семантика редукции
- 2.2 Семантика больших шагов
  - 2.2.1 Естественная семантика
3 Сравнение
4 См. Также
5 Ссылки
6 Внешние ссылки

История

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

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

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

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

Подходы

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

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

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

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

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

$⟨E, s⟩ ⇒ V ⟨L: = E, s⟩ ⟶ (s ⊎ (L ↦ V)) {\ displaystyle {\ frac {\ langle E, s \ rangle \ Rightarrow V} {\ langle L: = E \,, \, s \ rangle \ longrightarrow (s \ uplus (L \ mapsto V))}}}$ ${\ frac {\ langle E, s \ rangle \ Rightarrow V} {\ langle L: = E \,, \, s \ rangle \ longrightarrow (s \ uplus (L \ mapsto V))}}$

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

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

$⟨C 1, s⟩ ⟶ s ′ ⟨C 1; C 2, s ⟶ C 2, s ′⟩ ⟨C 1, s⟩ ⟶ ⟨C 1 ′, s ′⟩ C 1; C 2, s ⟶ ⟨C 1 '; C 2, s ′⟩ ⟨пропустить, s⟩ ⟶ s {\ 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}}}$ ${\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}}$

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

Если у нас также есть логические выражения для состояния, диапазон которых составляет $B {\ displaystyle B}$ $B$ , то мы можем определить семантику while команда: $⟨B, s⟩ ⇒ true ⟨, а B выполняет C, s⟩ ⟶ ⟨C; в то время как B делает C, s⟩ ⟨B, s⟩ ⇒ false ⟨, а B делает C, s⟩ ⟶ s {\ 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}}}$ ${\ 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 приобрела большую популярность и фактически стала стандартом в определении операционной семантики. Признаком успеха является то, что первоначальный отчет (так называемый Орхусский отчет) о SOS (Plotkin81) привлек более 1000 ссылок, согласно CiteSeer [1], что делает его одним из из наиболее цитируемых технических отчетов в Computer Science.

Семантика сокращения

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

$e = v | (e e) | х v = λ х. e C = [] | (C e) | (v C) {\ displaystyle e = v \; | \; (e \; e) \; | \; x \ quad \ quad v = \ lambda xe \ quad \ quad C = \ left [\, \ right] \; | \; (C \; e) \; | \; (v \; C)}$ $e = v \ ; | \; (e \; e) \; | \; x \ quad \ quad v = \ lambda xe \ quad \ quad C = \ left [\, \ right] \; | \; (C \; e) \; | \; (v \; C)$

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

$(λ x. E) v ⟶ e [x / v] (β) {\ displaystyle (\ lambda xe) \; v \ longrightarrow e \, \ left [x / v \ right] \ quad (\ mathrm {\ beta})}$ ${\ displaystyle (\ lambda xe) \; v \ longrightarrow e \, \ left [ x / v \ right] \ quad (\ mathrm {\ beta})}$

Эта единственная аксиома является бета-правилом из лямбда-исчисления. Контексты редукции показывают, как это правило сочетается с более сложными терминами. В частности, это правило может срабатывать для позиции аргумента приложения, например $((λ x. X λ x. X) λ x. (Xx)) {\ displaystyle ((\ lambda xx \; \ lambda xx) \ lambda x. (x \; x))}$ $((\ lambda xx \; \ lambda xx) \ lambda x. (x \; x))$ , потому что существует контекст $([] λ x. (xx)) {\ displaystyle ([\,] \; \ lambda x. (x \; x))}$ $([\,] \; \ lambda x. (x \; x))$ , который соответствует термину. В этом случае контексты однозначно разлагают термины, так что на любом данном шаге возможна только одна редукция. Расширение аксиомы для соответствия контекстам редукции дает совместимое замыкание. Рефлексивное, транзитивное замыкание этого отношения дает отношение редукции для этого языка.

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

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

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

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

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

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

Сравнение

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

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

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

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

См. Также

Ссылки

Жиль Кан. «Естественная семантика». Материалы 4-го ежегодного симпозиума по теоретическим аспектам информатики. Springer-Verlag. Лондон. 1987.
Гордон Д. Плоткин. Структурный подход к операционной семантике. (1981) Tech. Представитель DAIMI FN-19, факультет компьютерных наук, Орхусский университет, Орхус, Дания. (Перепечатано с исправлениями в J. Log. Algebr. Program. 60-61: 17-139 (2004), препринт ).
Гордон Д. Плоткин. Истоки структурной операционной семантики. J. Log. Algebr. Программа. 60-61: 3-15, 2004. (препринт ).
Дана С. Скотт. Обзор математической теории вычислений, Группа исследования программирования, Техническая монография PRG – 2, Оксфордский университет, 1970.
Адриан ван Вейнгаарден и др. Пересмотренный отчет об алгоритмическом языке ALGOL 68. IFIP. 1968. ([2] )
Мэтью Хеннесси. Семантика языков программирования. Wiley, 1990. доступно в Интернете.

Внешние ссылки

СМИ, связанные с Operational семантика в Wikimedia Commons