Операционная семантика. Изучение процесса спецификации программы с помощью операционной семантики (Лабораторная работа № 4)

Лабораторная работа № 4. Операционная семантика

Цель работы

Целью работы является практическое изучение процесса спецификации программы с помощью операционной семантики.

Содержание отчета

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

1.  Титульный лист.

2.  Цель работы.

3.  Текст задания.

4.  Решение задачи, представленное с помощью языка ПЯК.

5.  Пример выполнения разработанной ПЯК-программы на SMS-машине с обоснованием выбора входных данных.

6.  Выводы.

Теоретические сведения

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

1)  абстракция вычислительной машины;

2)  математические функции;

3)  математическая логика.

На основе этих смысловых областей и способов отображения синтаксиса языка на них были сформированы следующие виды семантик:

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

2)  Денотационная семантика.

3)  Аксиоматическая семантика.

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

Система переходов

Система переходов имеет две составляющие – множество конфигураций (состояний)  и бинарное отношение .

Определение 1. Термины и условные обозначения системы переходов .

1)  обозначает бинарное отношение на множестве , которое является рефлексивно-транзитивным замыканием отношения . Другими словами, отношение  имеет место только в том случае, если

имеет место для некоторой последовательности , где , а ситуация  интерпретируется как .

2)  обозначает, что не существует такого состояния , для которого имеет место .

3) система переходов называется детерминированной, если для любых  имеет место

(иногда используют термин «моногенная»).

4) часто и множества  выделяются подмножества  и , содержащие элементы, которые называются начальными и конечными состояниями соответственно. Тогда пара  представляет выполнение системы переходов. При этом если  тогда . Состояния, удовлетворяющие условию , называются отказами.

Абстрактная машина

Исторически, первый подход к выработке математически строгой операционной семантики программных языков был реализован в терминах абстрактной машины – системы переходов, определяющей интерпретатор языка. Рассмотрим пример, иллюстрирующий данный подход применительно к языку, который назовем простым языком команд (ПЯК). Мы будем использовать абстрактную машину, которая часто называется SMC-машиной. Возникновение данного имени обусловлено тем, что конфигурация машины может быть описана как тройка , где  - стек (промежуточных или конечных) результатов,  - память, то есть отображение множества целых чисел на некоторое конечное множество адресов, а  - управляющий стек выражений, подлежащих разбору. Перейдем к описанию языка ПЯК.

Синтаксис языка ПЯК

Выражения

Команды

Целочисленные выражения

Логические выражения

Вспомогательные определения:

 - множество целых чисел;

 - множество логических значений;

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

 - постоянное конечное множество целочисленных бинарных операций;

 - постоянное конечное множество логических бинарных операций.

ПЯК является довольно простым для описания языком. Реализация числовых алгоритмов с помощью этого языка основывается на управлении изменением состояний. В этом контексте мы можем считать, что состояние инкапсулирует конечное число адресов (регистров), в которых хранятся целые числа. Целочисленные и логические выражения описывают целые и логические значения, независящие от состояния. Команды ПЯК описывают операции изменения состояний.

SMC-машина

Конфигурация

Управляющий стек

Стек (промежуточных и конечных) результатов

Память состояний

 - частичная функция, отображающая адреса на целые числа, определенная только на конечном множестве адресов.

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

Определим начальные конфигурации в форме , где  - команда ПЯК, а  - состояние. Определим также конечные конфигурации как . Выполнение ПЯК-программы на SMC-машине описывается выражением , которое означает, что успешное выполнение команды  в состоянии  влечет переводит SMC-машине в состояние .