Лекция RAISE Development Method: некоторые виды спецификаций и проверка согласованности моделей
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко План лекции Общая идея RAISE метода Спецификация сигнатур Алгебраическая спецификация Моделе-ориентированная спецификация Отношение уточнения (refinement) Техника re-writing проверки согласованности моделей Пример проверки согласованности
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко RAISE Development Method – основные идеи Разработка разбивается на шаги Сначала описывается максимально простая и абстрактная модель На каждом шаге строится более подробная и конкретная модель На каждом шаге проверяется согласованность моделей
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко RAISE Development Method – шаги процесса разработки Шаг 0: объявление сорт-типов и определение сигнатур операций Шаг 1: аксиомы, алгебраическая спецификация Шаг 2.1: структуры данных и раздельные спецификации для каждой операции (имплицитные и эксплицитные), доказательство согласованности спецификаций шага 2.1 и шага 1... Шаг 2.i: детализация и расширение спецификаций предыдущего шага и доказательство согласованности с предыдущим шагом и с шагом 1. В конце возможна даже трансляция в код на языке программирования.
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко Спецификация сигнатур. Пример ABS_DATABASE = class type Database, Key, Data value empty : Database, insert : Key > Database, remove : Key > Database, defined : Key > Bool, lookup : Key > Data end
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко Спецификация сигнатур Объявления типов данных (так называемые сорт-типы) Сигнатуры операций (для некоторых операций сразу можно указать, что они не являются тотальными) Один из типов часто играет особую роль – целевой, то есть тот, который моделирует реализацию целевой системы (в данном примере – Database )
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко Виды операций Операции разделяются на два класса по их отношению к целевому типу: генераторы – целевой тип встречается среди выходных параметров ( empty, insert, remove) обсерверы (наблюдатели, observers) – целевой тип только среди входных параметров ( defined, lookup)
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко Виды операций (замечание) Иногда из множества генераторов выделяют минимальное подмножество операций, при помощи которых можно получить любое значение целевого типа, и только эти операции называют генераторами, а остальные – трансформерами (transformers) или преобразователями.
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко Алгебраическая спецификация DATABASE = class type Database, Key, Data value empty : Database, insert : Key> Database, remove : Key > Database, defined : Key > Bool, lookup : Key > Data
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко Алгебраическая спецификация (продолжение 1) axiom [ defined empty ] all k:Key :- defined(k,empty) == false, [ defined insert ] all k,k1:Key, d:Data, db:Database :- defined(k,insert(k1,d,db)) == k = k1 \/ defined(k,db), [ defined remove ] all k,k1:Key, db:Database :- defined(k,remove(k1,db)) == k ~= k1 /\ defined(k,db),
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко Алгебраическая спецификация (продолжение 2) [ lookup insert ] all k,k1:Key, d:Data, db:Database :- lookup(k,insert(k1,d,db)) == 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)) == lookup(k,db) pre k ~= k1 /\ defined(k,db) end
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко Алгебраическая спецификация Общее с спецификацией сигнатур: Декларации типов данных как сорт- типов Сигнатуры операций Отличие от абстрактной спецификации: Набор аксиом, связывающих последовательности операций
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко Полнота набора аксиом На практике в большинстве случаев достаточно написать аксиомы для пар операций генератор / обсервер трансформер / обсервер
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко SET_DATABASE = class type Key, Data, Record = Key > Bool is_wf_Database(rs) is (all k : Key, d1,d2 : Data :- ( (k,d1) isin rs /\ (k,d2) isin rs) => d1 = d2 ), empty : Database = {}, Моделе-ориентированная спецификация Database = Recordset
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко Моделе-ориентированная спецификация (продолжение) insert : Key > Database insert(k,d,db) is remove(k,db) union {(k,d)}, remove : Key > Database remove(k,db) is db \ {(k,d) | d : Data :- true}, defined : Key > Bool defined(k,db) is (exists d : Data :- (k,d) isin db), lookup : Key > Data lookup(k,db) as d post (k,d) isin db pre defined(k,db) end
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко Моделе-ориентированная спецификация Определения типов данных (хотя, возможно, не всех), часто как подтипы и/или при помощи вспомогательных функций (is_wf_…) Имплицитные или эксплицитные спецификации операций
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко Отношение уточнения (refinement) Две схемы находятся в отношении «одна уточняет или реализует другую» (refinement или implementation), если реализация сохраняет объявления всех сущностей, объявленных в абстрактной схеме, при этом сорт типы могут заменяться описанием типа подтипы могут заменяться своими максимальными типами могут появляться объявления и описания новых сущностей и свойств все свойства (аксиомы) абстракной спецификации справедливы в реализации
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко Доказательство согласованности двух спецификаций (доказательство отношения «уточняет») состоит из цепочки вида цель 1 аргументация цель n аргументация n Техника re-writing проверки согласованности моделей Аргументация – это ссылка на правила re-writing, см. The RAISE Development Method.
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко Пример («реализация») SET_DATABASE = class type Record = Key >< Data, Database = {| rs : Record-set :- is_wf_Database(rs) |}, Key, Data value is_wf_Database : Record-set -> Bool, empty : Database, insert : Key > Database, remove : Key > Database, defined : Key > Bool, lookup : Key > Data axiom forall k : Key, d : data, rs : Record-set, db : Database :- is_wf_Database(rs) is (all k : Key, d1, d2 : Data :- ((k,d1) isin rs /\ (k,d2) isin rs) => d1 = d2), empty is {}, insert(k,d,db) is remove(k,db) union {(k,d)}, remove(k,db) is db \ {(k,d) | d : Data :- db), defined(k,db) is (exists d : Data :- (k,d) isin db), lookup(k,db) as d post (k,d) isin db pre defined(k,db) end
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко Пример (алгебраическая спецификация) DATABASE = class type Record,Database,Key, Data value empty : Database, insert : Key > Database, remove : Key > Database, defined : Key > Bool, lookup : Key > Data axiom [ defined empty ] all k:Key :- defined(k,empty) == false, [ defined insert ] all k,k1:Key, d:Data, db:Database :- defined(k,insert(k1,d,db)) == k = k1 \/ defined(k,db), [ defined remove ] all k,k1:Key, db:Database :- defined(k,remove(k1,db)) == k ~= k1 /\ defined(k,db), [ lookup insert ] all k,k1:Key, d:Data, db:Database :- lookup(k,insert(k1,d,db)) == 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)) == lookup(k,db) pre k ~= k1 /\ defined(k,db) end
ВМиК МГУ, сентябрь-декабрь 2001 Формальные спецификации программ-I, Лекция 5. А.К.Петренко Пример (доказательство корректности уточнения) SET_DATABASE реализует DATABASE поскольку: 1. - SET_DATABASE определяет все типы, опреденные в DATABASE SET_DATABASE определяет все константы и функции, определенные в DATABASE, и определяет их с такими же сигнатурами Все аксиомы из DATABASE истинны в SET_DATABASE. Пример доказательства для аксиомы [defined_empty] [[defined(k,empty) is false]] unfold empty: [[defined(k,{}) is false]] unfold defined: [[(exists d : Data :- (k,d) isin {}) is false]] isin_empty: [[exists d : Data :- false) is false]] exists_introduction: [[false is false]] is_annihilation: [[true]] qed