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

Категория формальной семантики языка программирования

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

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

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

История

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

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

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

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

Подходы

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

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

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

Структурная операционная семантика (SOS, также называемая структурированной операционной семантикой или семантикой малых шагов ) была введена Гордоном Плоткиным в (Plotkin81) как логическое средство определения операционной семантики. Основная идея SOS состоит в том, чтобы определить поведение программы с точки зрения поведения ее частей, обеспечивая тем самым структурный, т. е. синтаксически-ориентированный и индуктивный взгляд на операционную семантику. Спецификация SOS определяет поведение программы с точки зрения (набора) переходных отношений . Спецификации 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}}$

Если у нас также есть логические выражения для состояния, ранжированные по , тогда мы можем определить семантику команды 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], что сделало его одним из наиболее цитируемых технических отчетов в области компьютерных наук .

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

Семантика редукции — это альтернативное представление операционной семантики. Его ключевые идеи были впервые применены к чисто функциональному вызову по имени и вариантам вызова по значению лямбда-исчисления Гордоном Плоткиным в 1975 году ^[3] и обобщены на функциональные языки более высокого порядка с императивными особенностями Матиасом Феллейзеном в его диссертации 1987 года. ^[4] В дальнейшем этот метод был развит Маттиасом Феллейзеном и Робертом Хибом в 1992 году в полностью эквациональную теорию управления и состояния . ^[2] Сама фраза «семантика редукции» была впервые использована Феллейзеном и Дэниелом П. Фридманом в статье PARLE 1987 года. ^[5]

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

${\displaystyle \mathbf {let\ rec} \ x=v_{1}\ \mathbf {in} \ x\leftarrow v_{2};\ e\ \ \longrightarrow \ \ \mathbf {let\ rec} \ x=v_{2}\ \mathbf {in} \ e}$

Чтобы поставить оператор присваивания в такую ​​позицию, он «всплывает» через функциональные приложения и правую часть операторов присваивания, пока не достигнет нужной точки. Поскольку промежуточные выражения могут объявлять разные переменные, исчисление также требует правила вытягивания для выражений. Большинство опубликованных вариантов использования семантики сокращения определяют такие «пузырьковые правила» с удобством контекстов оценки. Например, грамматика контекстов оценки в простом языке вызова по значению может быть задана как ${\displaystyle \mathbf {let} }$ ${\displaystyle \mathbf {let} }$

${\displaystyle E::=[\,]\ {\big |}\ v\ E\ {\big |}\ E\ e\ {\big |}\ x\leftarrow E\ {\big |}\ \mathbf {let\ rec} \ x=v\ \mathbf {in} \ E\ {\big |}\ E;\ e}$

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

${\displaystyle E[\,x\leftarrow v;\ e\,]\ \ \longrightarrow \ \ x\leftarrow v;\ E[\,e\,]\qquad {\text{(lift assignments)}}}$

Это единственное правило сокращения представляет собой правило подъема из лямбда-исчисления Феллизена и Хиба для операторов присваивания. Контексты оценки ограничивают это правило определенными терминами, но оно свободно применимо к любому термину, в том числе к лямбда-выражениям.

Следуя Плоткину, демонстрация полезности исчисления, полученного на основе набора правил редукции, требует (1) леммы Чёрча-Россера для одношагового отношения, которая порождает оценочную функцию, и (2) леммы стандартизации Карри-Фейса для транзитивно-рефлексивное замыкание одношагового отношения, которое заменяет недетерминированный поиск в оценочной функции на детерминированный крайний левый/крайний поиск. Феляйзен показал, что императивные расширения этого исчисления удовлетворяют этим теоремам. Следствием этих теорем является то, что эквациональная теория — симметрично-транзитивно-рефлексивное замыкание — является здравым принципом рассуждения для этих языков. Однако на практике большинство приложений семантики редукции обходятся без исчисления и используют только стандартную редукцию (и вычислитель, который может быть получен из нее).

Семантика редукции особенно полезна, учитывая легкость, с которой контексты оценки могут моделировать состояние или необычные конструкции управления (например, первоклассные продолжения ). Кроме того, семантика редукции использовалась для моделирования объектно-ориентированных языков, ^[6] контрактных систем , исключений, фьючерсов, вызова по необходимости и многих других особенностей языка. Тщательное современное рассмотрение редукционной семантики, в котором подробно обсуждаются несколько таких приложений, представлено Маттиасом Феллейзеном, Робертом Брюсом Финдлером и Мэтью Флэттом из отдела семантической инженерии с PLT Redex . ^[7]

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

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

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

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

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

Сравнение

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

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

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

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

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

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

Рекомендации

1. Маккарти, Джон . «Рекурсивные функции символьных выражений и их машинное вычисление, часть I». Архивировано из оригинала 4 октября 2013 г. Проверено 13 октября 2006 г.
2. Феллейзен, М.; Хиеб, Р. (1992). «Пересмотренный отчет о синтаксических теориях последовательного управления и состояния». Теоретическая информатика . 103 (2): 235–271. дои : 10.1016/0304-3975(92)90014-7.
3. Плоткин, Гордон (1975). «Вызов по имени, вызов по значению и λ-исчисление» (PDF) . Теоретическая информатика . 1 (2): 125–159. дои : 10.1016/0304-3975(75)90017-1 . Проверено 22 июля 2021 г.
4. Феллизен, Матиас (1987). Исчисления преобразования Lambda-v-CS: синтаксическая теория управления и состояния в императивных языках программирования высшего порядка (PDF) (доктор философии). Университет Индианы . Проверено 22 июля 2021 г.
5. Феллизен, Матиас; Фридман, Дэниел П. (1987). «Семантика редукции для императивных языков высшего порядка». Труды параллельных архитектур и языков Европы . Международная конференция по параллельным архитектурам и языкам в Европе. Том. 1. Шпрингер-Верлаг. стр. 206–223. дои : 10.1007/3-540-17945-3_12.
6. Абади, М.; Карделли, Л. (8 сентября 2012 г.). Теория объектов. ISBN 9781441985989.
7. Феллизен, Матиас; Финдлер, Роберт Брюс; Флэтт, Мэтью (2009). Семантическая инженерия с PLT Redex. Массачусетский технологический институт Пресс. ISBN 978-0-262-06275-6.
8. Университет Иллинойса CS422
9. Ксавье Лерой . «Коиндуктивная операционная семантика большого шага».

дальнейшее чтение

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

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

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