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

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

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

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

История [ править ]

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

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

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

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

Подходы [ править ]

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

Семантика малых шагов [ править ]

Структурная операционная семантика [ править ]

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

В качестве простого примера мы рассмотрим часть семантики простого языка программирования; соответствующие иллюстрации приведены в Plotkin81 и Hennessy90 и других учебниках. Позвольте перемещаться по программам языка и позволять изменять состояния (например, функции от ячеек памяти до значений). Если у нас есть выражения (в диапазоне от ), values ( ) и location ( ), то команда обновления памяти будет иметь семантику:${\ 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}}$

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

Семантика редукции [ править ]

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

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

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

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

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

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

Семантика большого шага [ править ]

Естественная семантика [ править ]

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

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

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

Сравнение [ править ]

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

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

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

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

См. Также [ править ]

• Алгебраическая семантика
• Аксиоматическая семантика
• Денотационная семантика
• Формальная семантика языков программирования

Ссылки [ править ]

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

Внешние ссылки [ править ]

• СМИ, связанные с операционной семантикой, на Викискладе?