Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL (Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL.pdf), страница 7

При этомсреди объявленных типов особо выделяется тип, с помощью которогомоделируется реализация целевой системы, - целевой тип.В качестве примера рассмотрим разработку алгебраической спецификациипростейшей СУБД со следующей функциональностью. База данных представляетсобой набор записей, имеющих ключ и значение, причем каждое значение ключадолжно встречаться в базе не более одного раза (свойство уникальности ключа).Система должна обеспечивать возможность добавления записи, удаления записи поключу, проверки наличия в базе записи с заданным значением ключа, а такжепоиска значения по ключу, если запись с таким ключом имеется в базе.Можно предложить следующую спецификацию сигнатур для данной системы:DATABASE =classtype Database, Key, Datavalue/∗ пустая база данных∗/empty : Database,/∗ добавление записи в базу данных∗/insert : Key><Data><Database-> Database,/∗ удаление записи с указанным ключом из базы данных∗/remove : Key >< Database -> Database,/∗ проверка наличия в базе данных записи с заданным ключом ∗/defined : Key >< Database -> Bool,/∗ поиск значения по ключу, если запись с таким ключом в базе есть∗/lookup : Key >< Database -~-> Dataend35Целевым типом предложенной спецификации является тип 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.36Итак, общая схема построения алгебраической спецификации:1.

специфицировать сигнатуры функций,2. выделить генераторы и обсерверы,3. составить набор аксиом для пар вида обсервер/генератор иобсервер/модификатор.Для рассмотренного примера получим следующую алгебраическуюспецификацию:scheme DATABASE =classtype Database, Key, Datavalueempty : Database,insert : Key><Data><Database-> Database,remove : Key >< Database -> Database,defined : Key >< Database -> Bool,lookup : Key >< Database -~-> Dataaxiom[ 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)) isk = k1 \/ defined(k,db),[ defined_remove ]all k,k1:Key, db:Database :defined(k,remove(k1,db)) isk ~= k1 /\ defined(k,db),[ lookup_insert ]all k,k1:Key, d:Data, db:Database :lookup(k,insert(k1,d,db)) isif k = k1 then delse lookup(k,db) endpre k = k1 \/ defined(k,db),[ lookup_remove ]all k,k1:Key, db:Database :lookup(k,remove(k1,db)) islookup(k,db)pre k ~= k1 /\ defined(k,db)endRAISE метод разработки программ.

Понятие уточнения моделейРазработка программных систем методом RAISE базируется на парадигмепоследовательного уточнения. Общая идея заключается в следующем:•Разработка разбивается на шаги•Сначала описывается максимально простая и абстрактная модель•На каждом шаге строится более подробная и конкретная модель•На каждом шаге проверяется согласованность моделейТаким образом, разработка идет сверху вниз по шагам, от более абстрактныхмоделей к более конкретным. Процесс перехода от одной абстрактной модели к37другой называется уточнением (refinement), полученная в результате уточнениямодель называется реализацией.

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

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

правила вывода - набор теорем для выполнения:• тождественных преобразований,• преобразований кванторов,2. подстановки - раскрытие идентификаторов и т.д.,3. вычисление выражений.Доказательство согласованности двух спецификаций (доказательствоотношения «уточняет») для каждого свойства исходной модели представляет собойцепочку вида:цель1[[аргументация1]]…цельn[[аргументацияn]],где очередная цель задает доказываемое свойство, аргументация задает ссылку наприменяемое на данном шаге доказательства правило. Любая следующая цель вэтой цепочке является результатом преобразования предыдущей цели всоответствии с указанным правилом.38В качестве примера рассмотрим доказательство справедливости аксиомы[defined_empty] для модели-реализации, где база данных моделируется в видемножества записей со следующим определением константы empty и функцииdefined:empty : Database = { },defined : Key >< Database -> Booldefined(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.