Основы программирования

Лекция 5 - Аксиоматическая семантика
Индекс материала
Лекция 5
Метод таблиц решений
Операционная семантика
Денотационная семантика
Аксиоматическая семантика
Аксиоматическая семантика1
Все страницы

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

 

В аксиоматической семантике алгебраического подхода система (5) интерпретируется как набор аксиом в рамках некоторой формальной логической системы, в которой есть правила вывода и / или интерпретации определяемых объектов.

Для интерпретации системы (1) вводится понятие аксиоматического описания (S, E) — логически связанной пары понятий: S — сигнатура используемых в системе (1) символов функций f1, f2, ..., fm и символов констант (нульместных функциональных символов) c1, c2, ..., cm, а E — набор аксиом, представленный системой (1). Предполагается, что каждая переменная xi, i = 1, ..., k, и каждая константа cj, j =1, ..., l, используемая в E, принадлежит к какому-либо из типов данных t1, t2, ..., tr, а каждый символ fi, i =1, ..., m, представляет функцию, типа

ti1 * ti2 * ... * tik → ti0.

Такое аксиоматическое описание получит конкретную интерпретацию, если будут заданы конкретные типы данных ti = t′i, i = 1, ..., r, и конкретные значения констант ci = c′i, i = 1, ..., l. В таком случае говорят, что задана одна конкретная интерпретация A символов сигнатуры S, называемая алгебраической системой

A = (t′1, ..., t′r, f ′1, ..., f ′r, с′1, ..., с′ r),

где f ′i, i = 1, ..., m, конкретная функция, представляющая символ fi. Таким образом, аксиоматическое описание (S, E) определяет класс алгебраических систем (частный случай: одну алгебраическую систему), удовлетворяющих системе аксиом E, т.е. превращающих равенства системы E в тождества после подстановки в них f ′i, i = 1, ..., m, и ci = c′i, i = 1, ..., l, вместо fi и ci соответственно.

В программировании в качестве алгебраической системы можно рассматривать, например, тип данных, при этом определяемые функции представляют операции, применимые к данным этого типа. Так К. Хоор построил аксиоматическое определение набора типов данных [4], которые потом Н. Вирт использовал при создании языка Паскаль.

В качестве примера рассмотрим систему равенств:

УДАЛИТЬ(ДОБАВИТЬ(m,d))=m,

ВЕРХ(ДОБАВИТЬ(m,d))=d,

УДАЛИТЬ(ПУСТ)=ПУСТ,

ВЕРХ(ПУСТ)=ДНО,

где УДАЛИТЬ, ДОБАВИТЬ, ВЕРХ — символы функций, а ПУСТ и ДНО — символы констант, образующие сигнатуру этой системы. Пусть D, D1 и М — некоторые типы данных, такие, что mM, dD, ПУСТM, ДНО D1, а функциональные символы представляют функции следующих типов:

УДАЛИТЬ: M → M,

ДОБАВИТЬ: M * D → M,

ВЕРХ: M → D1.

Данная сигнатура вместе с указанной системой равенств, рассматриваемой как набор аксиом, образует некоторое аксиоматическое описание.

С помощью этого аксиоматического описания определим абстрактный тип данных, называемый магазином, задав следующую интерпретацию символов её сигнатуры: пусть D — множество значений, которые могут быть элементами магазина, D1 = D | {ДНО}, а M — множество состояний магазина,

M = {d1, d2, ..., dn | dniD, i = 1, ..., n, ni0},

ПУСТ = {}, ДНО — особое значение (зависящее от реализации магазина), не принадлежащее D. Тогда указанный набор аксиом определяют свойства магазина.

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