 пустая база данных

empty : Database,

 добавление записи в базу данных

insert : Key><Data><Database-> Database,

 удаление записи с указанным ключом из базы данных

remove : Key >< Database -> Database,

 проверка наличия в базе данных записи с заданным ключом 

defined : Key >< Database -> Bool,

 поиск значения по ключу, если запись с таким ключом в базе есть

lookup : Key >< Database -~-> Data

end

Целевым типом предложенной спецификации является тип Database.

Классификация функций модели на генераторы, модификаторы и обсерверы

На следующем шаге построения алгебраической спецификации осуществляется разбиение функций на два класса – генераторов (конструкторов) и обсерверов – в зависимости от их отношения к целевому типу. К классу генераторов (конструкторов) относятся функции, формирующие значения целевого типа. Формальным признаком таких функций является наличие целевого типа среди выходных параметров в сигнатуре функций. В рассмотренном примере этот класс функций представлен функциями empty, insert и remove. К классу обсерверов (от английского термина observers) относятся функции доступа к значениям целевого типа, возвращающие по значению целевого типа значения других типов. Такие функции не изменяют значения целевого типа. Формальным признаком обсерверов является наличие целевого типа только среди входных параметров. В рассмотренном примере этот класс функций представлен функциями defined и lookup.

Иногда из множества генераторов выделяют минимальное подмножество функций, при помощи которых можно получить любое значение целевого типа, и только эти функции называют генераторами или конструкторами, а остальные – модификаторами или преобразователями. Для нашего случая генераторами в этом понимании являются функции empty и insert, модификатором - remove. Действительно, любая база данных может быть представлена выражением вида:

insert(k1,d1,insert(k2,d2,...,insert(kn,dn,empty)...)),

т.е. может быть построена путем конечного числа применений функции insert к пустой базе данных.

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

Методика построения алгебраической спецификации

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

• обсервер / генератор,

• обсервер / модификатор.

Для полноты описания свойств целевого типа в ряде случаев рекомендуется расширить этот набор аксиомами для пар вида модификатор / генератор.

При составлении набора аксиом необходимо принимать во внимание возможную частичную определенность функций. Так, из-за частичной определенности функции lookup из состава аксиом следует исключить пару lookup(empty) и указать предусловие ко всем аксиомам с функцией lookup.

Итак, общая схема построения алгебраической спецификации:

1. специфицировать сигнатуры функций,

2. выделить генераторы и обсерверы,

3. составить набор аксиом для пар вида обсервер/генератор и обсервер/модификатор.

Для рассмотренного примера получим следующую алгебраическую спецификацию:

scheme DATABASE =

class

type Database, Key, Data

value

empty : Database,

insert : Key><Data><Database-> Database,

remove : Key >< Database -> Database,

defined : Key >< Database -> Bool,

lookup : Key >< Database -~-> Data

axiom

[ defined_empty ]

all k:Key :-

defined(k,empty) is false,

[ defined_insert ]

all k,k1:Key, d:Data, db:Database :-

defined(k,insert(k1,d,db)) is

k = k1 \/ defined(k,db),

[ defined_remove ]

all k,k1:Key, db:Database :-

defined(k,remove(k1,db)) is

k ~= k1 /\ defined(k,db),

[ lookup_insert ]

all k,k1:Key, d:Data, db:Database :-

lookup(k,insert(k1,d,db)) is

if k = k1 then d

else lookup(k,db) end

pre k = k1 \/ defined(k,db),

[ lookup_remove ]

all k,k1:Key, db:Database :-

lookup(k,remove(k1,db)) is

lookup(k,db)

pre k ~= k1 /\ defined(k,db)

end

RAISE метод разработки программ. Понятие уточнения моделей

Разработка программных систем методом RAISE базируется на парадигме последовательного уточнения. Общая идея заключается в следующем:

• Разработка разбивается на шаги

• Сначала описывается максимально простая и абстрактная модель

• На каждом шаге строится более подробная и конкретная модель

• На каждом шаге проверяется согласованность моделей

Таким образом, разработка идет сверху вниз по шагам, от более абстрактных моделей к более конкретным. Процесс перехода от одной абстрактной модели к другой называется уточнением (refinement), полученная в результате уточнения модель называется реализацией. При этом говорят, что одна спецификация уточняет другую, если:

• реализация сохраняет объявления всех сущностей исходной спецификации (абстрактные типы могут заменяться описанием типа, подтипы могут заменяться своими максимальными типами),

• могут появляться объявления и описания новых сущностей и свойств,

• все свойства (аксиомы) исходной спецификации остаются справедливыми в реализации.

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

RAISE метод предполагает следующую последовательность разработки спецификаций. На первом шаге строится алгебраическая спецификация системы, оперирующая абстрактными типами данных, далее выполняется уточнение используемых типов и построение раздельных спецификаций для функций системы. Таким образом, в зависимости от выбранного yточнения типов строится та или иная моделе-ориентированная спецификация системы, оперирующая уже конкретными типами данных. При этом, как правило, сначала строится неявная спецификация функций системы, затем явная. На заключительном этапе разработки возможна автоматическая кодогенерация в целевой язык программирования.

Проверка согласованности моделей

Для проверки согласованности уточнения необходимо убедиться, что все свойства (аксиомы) исходной модели остаются справедливыми в уточненной модели. Для этого в RAISE применяется техника re-writing формального доказательства, базирующаяся на следующих механизмах

1. правила вывода - набор теорем для выполнения

• тождественных преобразований,

• преобразований кванторов,

1. подстановки - раскрытие идентификаторов и т.д.,

2. вычисление выражений.

Доказательство согласованности двух спецификаций (доказательство отношения «уточняет») для каждого свойства исходной модели представляет собой цепочку вида:

цель₁

[[аргументация₁]]

…

цель_n

[[аргументация_n]],

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

В качестве примера рассмотрим доказательство справедливости аксиомы [defined_empty] для модели-реализации, где база данных моделируется в виде множества записей со следующим определением константы empty и функции defined:

empty : Database = { },

defined : Key >< Database -> Bool

defined(k,db) is (exists d : Data :- (k,d) isin db)

Пример доказательства для аксиомы [defined_empty].

[ defined_empty ]

all k:Key :-

defined(k,empty) is false - исходная цель доказательства

[[раскрыть квантор]]

defined(k,empty) is false

[[раскрыть идентификатор empty]]

defined(k,{}) is false

[[раскрыть идентификатор defined]]

(exists d : Data :- (k,d) isin {}) is false

[[вычислить isin {}]]

(exists d : Data :- false) is false

[[преобразовать квантор]]

false is false

[[тождественное преобразование]]

true

Упражнения

1. Построить алгебраическую спецификацию стека со следующими функциями:

• поместить элемент в стек,

• удалить верхний элемент непустого стека,

• проверить стек на пустоту,

• найти значение верхнего элемента непустого стека (без удаления из стека).

1. Построить алгебраическую спецификацию очереди со следующими функциями:

• добавить элемент в очередь,

• удалить элемент из непустой очереди,

• проверить очередь на пустоту,

• найти значение первого элемента непустой очереди (без удаления из очереди),

• подсчитать количество элементов в очереди.

Указания: в упражнениях 1, 2 руководствуйтесь общей схемой построения алгебраической спецификации.

1. Используя абстракцию списков, уточнить построенную алгебраическую спецификацию стека в моделе-ориентированную спецификацию. Проверить согласованность уточнения.

1. Используя абстракцию списков, уточнить построенную алгебраическую спецификацию очереди в моделе-ориентированную спецификацию. Проверить согласованность уточнения.

1. Доказать, что вторая спецификация является (или не является) уточнением первой.

value

f1 : A >< L -~-> L,

f2 : A >< L -~->,

f3 : L -> Nat

axiom

all a : A, b : L :-

f3(f1(a,b)) is f3(b) + 1

pre f3(b) = 1,

all a : A, b : L :-

f3(f2(a,b)) is 1 + f3(b)

pre f3(b) = 1,

all a : A, b : L :-

f1(a,b) is f2(a,b)

pre f3(b) = 1

type

L = A-list

value

f1 : A >< L -~-> L

f1(a,b) is <. a .> ^ tl b

pre b ~= <..>,

f2 : A >< L -~-> L

f2(a,b) is tl b ^ <. a .>

pre b ~= <..>,

f3 : L -> Nat

f3(ls) is len ls

ГЛАВА 7. ВАРИАНТНЫЕ ОПРЕДЕЛЕНИЯ

Понятие вариантного определения. Виды вариантных определений. Конструкторы, деструкторы и реконструкторы. Упражнения.

Понятие вариантного определения

Вариантное определение (определение вариантного типа) задается конструкцией вида:

type id = = variant₁ | ... | variant_n , n  1

и предназначено для удобного и компактного определения абстрактного типа (id) вместе с набором функций и констант над этим типом. Т.е. вариантное определение представляет собой сокращенную форму записи определения абстрактного типа, определения некоторых функций и аксиом. Среди определяемых функций могут быть:

• конструкторы – для генерации значений данного типа,

• деструкторы – для декомпозиции значений данного типа,

• реконструкторы – для модификации значений данного типа.

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

Виды вариантных определений. Конструкторы, деструкторы и реконструкторы

Конструкторы-константы

Простейшим видом вариантного определения является использование конструкторов-констант, когда тип определяется путем явного перечисления его значений. В качестве примера рассмотрим вариантное определение:

type Colour = = black | white

Оно представляет собой сокращенную форму записи следующего фрагмента спецификации:

type Colour /* объявление абстрактного типа */

value

black : Colour, /* определение констант */

white : Colour

axiom

[ disjoint ]

black ~= white,

[ induction ]

all p : Colour -> Bool :- (p(black) /\ p(white)) => (all с : Colour :- p(c))

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

Конструкторы записей

Более сложным видом вариантного определения является использование в качестве конструкторов функций для генерации значений определяемого типа - конструкторов записей (record constructions). Такие конструкторы используются при определении структур данных. В частности, эти конструкторы могут использоваться для генерации записей, где под записью подразумевается набор именованных полей.

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

type Collection = = empty | add(Elem, Collection),

в котором используется конструктор-константа empty и конструктор записи add. Это определение рекурсивно определяет тип Collection, содержащий два вида значений:

1. значение empty,

2. значения, построенные с помощью конструктора add.

Данное вариантное определение представляет собой сокращение следующего фрагмента спецификации: