СЕМАНТИКА АЛГОРИТМИЧЕСКИХ ЯЗЫКОВ
Семантика языка - это соответствие, сопоставляющее выражениям их денотат ... Такое определение семантики позволяет нам дать ответ на вопрос, когда семантика может считаться заданной, но полностью обходит вопрос, как ее задавать ... Конструктивное уточнение этого определения невозможно без уяснения цели, ради которой необходимо задать семантику языка ... Поскольку алгоритмический язык задает программы, которые должны исполняться, первым естественным ответом на вопрос, как задать его семантику, является: «Определить действие каждой конструкции» ... такое определение семантики необходимо нам, если мы ставим цель построить транслятор с данного языка. Это - операционная семантика, семантика типа «как работает программа». Такую семантику требует и инженер, желающий непосредственно «воплотить» наш язык в аппаратуре. Поэтому зачастую ответ на вопрос «как» и считается единственной задачей семантики ... Однако если смотреть на программу не как на объект трансляции, а как на устройство, выполняющее некоторую функцию, то необязательно знать, как она работает. Важно, что она сделает, каковы будут ее результаты ... Если же программы у нас еще нет, то нам нужно знать, чем и в каких случаях пользоваться для программирования, для построения программы, решающей нашу задачу ... семантика алгоритмического языка должна уметь отвечать на некоторые из вопросов: как работают программы, что они делают, чем пользоваться, чтобы их создать или изменить ... Идеальное описание алгоритмического языка должно было бы содержать: интерпретацию действия программы для системных программистов; интерпретацию содержательного смысла программы для пользователей, желающих прочитать и использовать чужую программу; правила построения программы и ее модификации (конструктивное описание). Все эти (как минимум, три: интерпретационное, функциональное и конструктивное) описания должны быть согласованы. Пока что ни один язык таким образом не описан ... Когда мы исследуем результаты действия программы, то на программу естественно смотреть как на функционал в некотором пространстве. Этот функционал может трактоваться как рекурсивная функция, если мы на первый план выдвигаем принципиальную ВЫЧИСЛИМОСТЬ, а не конкретные вычисления ... Семантику в терминах непрерывных решеток Скотта или другую форму денотационной семантики можно задавать, если мы исследуем структуру множества программ ... Если нас интересуют свойства данных, действие программы можно описывать как связь между входным и выходным условиями - это подход Флойда-Хоара ... Если нас интересуют чисто алгебраические соотношения между получающимися программами, то естественно описывать лишь взаимосвязи программ в виде некоторой системы тождеств или условных тождеств, и возникает современная теория абстрактных типов данных (АТД) и их инициальных моделей ... Если же нас интересуют алгебраические свойства одного множества программ в сопоставлении с другим (например, создаваемого пакета для обработки нового типа данных с уже существующими), то целесообразно использовать в качестве аппарата теорию категорий ... При описании действия программы мы сводим ее к композиции элементарных операций. Эти операции сами должны быть описаны, и здесь мы стоим перед выбором одной из четырех альтернатив: считать их заданными на некотором формальном алгоритмическом языке, который уже считается известным; считать, что на формальном логическом языке описаны их свойства; считать, что некоторым точным образом описаны функции, вычисляемые операциями; описать действие операций на некотором диалекте естественного языка ... Этот выбор может быть реализован разными способами ... проекционный подход к семантике (она определяется как соответствие между новым языком и известным), редукционный подход (частный случай проекционного), трансформационный, интерпретационный (когда язык заранее и навсегда фиксирован, как, например, VDL или язык Тузова). Все эти четыре направления в семантике: интерпретационные семантики ... примером описания семантик через композиции функционалов, интерпретирующих элементарные операции, служит VDM ... В теории схем программ и многих алгебраических семантиках программа определяется через историю применения элементарных операций, а смысл самих элементарных функций может варьироваться ... Когда описание операций логическое, мы представляем программу как преобразователь предикатов по Дейкстре ... Для конструктивных семантик нужно иметь либо хорошую систему преобразований программ (правила трансформации, алгебру программ либо категорные конструкции), либо систему индуктивного вывода программы ПО неполной информации, либо знания о том, как разбивать программу на части и собирать программу из кусков (композиционный подход, если описание правил композиции и декомпозиции носит алгоритмический характер, и логический, если нет ... важно для понимания то, что чему соответствует на практике и какие средства описания согласуются с тем или иным способом задания семантики (примеры и прагматика) ... Зачем нужна формальная семантика и нужна ли она? ... с точки зрения понимаемое™ человеком, и даже как спецификация для программирования, содержательное определение обычно не хуже формального. Неясно, что добавляет к нашему пониманию практического языка его длинное денотационное описание. Но уже создание транслятора или интерпретатора для алгоритмического языка неизбежно является формализацией его семантики ... но, формализуя, необходимо понимать, чего мы стремимся достичь этой формализацией ... Основным назначением теоретической формальной семантики является анализ концепций алгоритмического языка и проверка логичности и согласованности его определения ... список целей, которые можно ставить при формализации семантики: спецификация требований, анализ конструкций, методы анализа программ, методы трансформации и оптимизации программ, методы конструирования и трансформации программ при изменении целей, верификация функциональности и удобства новых методов, полное описание языка, конструирование теории ...
Н. Н. Непейвода, “Семантика алгоритмических языков”, Итоги науки и техн. Сер. Теор. вероятн. Мат. стат. Теор. кибернет., 20, ВИНИТИ, М., 1983, 95-166; J. Soviet Math., 25:6 (1984), 1558-1606
www.mathnet.ru