LecTP5 (1127816), страница 3

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 3)

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

M={d1, d2, ... , dn | di  D, i=1, ... , n, n0},

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

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

5.6. Языки спецификаций.

Как уже отмечалось, функциональная спецификация представляет собой математически точное, но, как правило, не формальное описание поведения ПС. Однако, формализованное представление функциональной спецификации имеет ряд достоинств, главным из которых является возможность применять некоторые виды автоматизированного контроля функциональной спецификации.

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

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

Упражнения к лекции 5.

1. Функции

function F(n: integer): integer;

function G(n: integer): integer;

определены с помощью операционной семантики равенствами:

F(0)=1,

G(0)=2,

F(n)=G(n-1),

G(n)=F(n-1) + G(n-1).

Найти значения F(3) и G(3).

1. Формальные языки E и T определены над алфавитом

{'a', '*', '&', '<', '>'}

с помощью денотационной семантики равенствами

E= T  '*' T  E '&' T

T= 'a'  'a*'  '<' E '>'

Какие из следующих строк

'*a&*a*&a*'

'*a&<a&a*>'

'*<*a*&a>&<*a*>*'

принадлежат языку E и какие не принадлежат.

1. Формальные языки E и T определены над алфавитом

{'a', '#', '*', '(', ')'}

с помощью денотационной семантики равенства

E= T  '#' T  '(' E ')' '*' T

T= 'a'  'a#'  E

Какие из следующих строк

'(#a)*##a

'##(a)#*a#'

'(a)*#(a#)*a#'

принадлежат языку E и какие не принадлежат.

5.4. Тип R определен с помощью следующей аксиоматической семантики.

Описания:

type R= record P1, P2, P3: CHAR end;

function READ(S: R): CHAR; {READ: R -> CHAR}

function SHIFT(S: R): R; {SHIFT: R -> R}

function ADD(S: R, C: CHAR): R; {ADD: R * CHAR -> R} function REMOVE(S: R): R; {REMOVE: R -> R}

var X, Y, Z: CHAR;

U: R;

Аксиомы:

SHIFT(ADD(ADD(ADD(U, X), Y), Z)) =

ADD(ADD(ADD(U,Y), Z), X);

REMOVE(U) = SHIFT(ADD(U, '#'));

READ(SHIFT(ADD(U, X))) = X;

Найти значение:

READ(SHIFT(SHIFT(REMOVE(ADD(ADD(U, 'a'), 'b'))))) =

Литература к лекции 5.

5.1. В.Н. Агафонов. Спецификация программ: понятийные средства и их организация. - Новосибирск: Наука (Сибирское отделение), 1987.

5.2. Ian Sommerville. Software Engineering. - Addison-Wesley Publishing Company, 1992.

5.3. Д. Скотт. Теория решеток, типы данных и семантика / Данные в языках программирования. - М.: Мир, 1982. - С. 25-53.

5.4. К. Хоор. О структурной организации данных / У. Дал, Э. Дейкстра, К. Хоор. Структурное программирование. - М.: Мир, 1975. - С. 98-197.

Характеристики

Список файлов лекций