МФСП, 05 семинар (от 29 сентября)
Материал из eSyr's wiki.
Алгебраические спецификации в RSL
Чстный случай аксиом. спецификации. Имеет след. собенности:
- На первом шаге фрм. абстрактные типы, с ктрым мы хтим рабтть, и целевй тип, кторый мделир. специфиц. систему.
- писываются сигнатуры функций. Тольк сигнтуры.
- Фрмулируются аксиомы специальнго вида: _i(f_i(x), ..., f_n(x)) &equal; expr. Это требуется для выявления свйств, не пр. их.
Пример:
type Key, Record, Database value empty : Database insert : Key × Record × Database → Database remove : Key × Database → с волной Database defined : Key × Database → Bool lookup : Key × Database → с волной Record
Мы прошли первых два этапа.
Для удобства принято выд. дв типа перций: генератор (операция, прим. ктрой позв. плучить любое знач. целевого типа). Тут их два: insert, empty. Генертры и среди перндов имеет целевй тип, и знач — цеевой тип. Операции, к-рые называются observer, не меняют целевй тип, а возвр. инф., связнную с ним. И модификторы. Частный случай генератора, но с пмощью них нельзя плучить любое знач. целевого типа. Но при этм они меняют цел. тип.
Для чег нужна эта классиф? Чтобы неким разумным обр. сформ. правила, по которым форм. аксимы нашей системы. бычно, дст. сфрм. аксиому для каждй пары observer-generator, observer-modificator. Иногда также бывает делть пльзено аксимы для связи modiicator-generator, они избыточны бычн, но нглядны.
Теперь будем выпис. аксиомы, удовл. нашей операции:
- defined_empty
- defined_insert
- defined_remove
- lookup_insert
- lookup_remove
lookup_empty — не имеет смысла, опущена.
Далее выпис. все аксимы, используя в кач. арг. раз. переменные, кторые потм змык. квантором всеобщности. Правя чсть аксиом пишется сотв. семнтике. Если функ. част. спец., т небх. опр. предусловия.
axiom
∀ k : Key • defined(k, empty) &equal; false
∀ k_1, k_2 : Key • ∀ r : Record • ∀ db : Database • defined(k_1, insert(k_2, r, db)) &equal; (k_1 = k_2) ∨ defined(k_1, db)
∀ k_1, k_2 : Key • ∀ db : Database • defined(k_1, remove(k_2, db)) &equal; (k_1 ≠ k_2) ∧ defined(k_1, db)
∀ k_1, k_2 : Key • ∀ r : Record • ∀ db : Database • lookup(k_1, insert(k_2, r, db)) &equal; if k_1 = k_2 then r else lookup(k_1, db)
pre (k_1 = k_2) ∨ defined(k_1, db)
∀ k_1, k_2 : Key • ∀ db : Database • lookup(k_1, remove(k_2, db)) &equal; lookup(k_1, db)
pre (k_1 ≠ k_2) ∧ defined(k_1, db)
Почему эт нз. алг. спец?
Потому что этот пдх из функ. пргр. Мы этими ксимми задаём алгебр. отношения.
Сам процесс проектирования программы в технологии RAISE.
- Формулировка типов. Выбор целевого типа
- Написание сигнатур. (Как в ООП: выбираем классы, и пишем методы)
- Формулируем аксиомы, связ. функции, исп. алг. подход. В рез-те получается алг. спецификация.
- После чего итерационно идёт пошаговая реализация.
- Уточнить тип
- Спецификация функции
- При этом необходимо соблюдать непротиворечивость исх. аксиом алг. спецификации.
Прверять каждую акс. и дказывать руками тяжело, есть авт. средства, но на практикуме оно не потребуется.
Пример (из примера пр БД): допустим, мы на некем шаге релиз. решили, что
type
Database = Key × Record-set
var
empty : Database = {}
defined(k,db) = ∃r : Record • (k, r) ∈ db
Теперь прверим, что специф. не пртивор. аксиоме:
[define_empty]
∀ k : Key • defined(k, empty) &equal; false
&fora;; k : Key • ∃r : Record • (k, r) ∈ {} &equal; false
У нас матлг был, метды резолюции знаем, всё очевидно. Левая часть тжд. равна false, false&equal;false, аксиома выполняется.
На практикуме форм. док. треб. не будет, но если бн. противоречие, то плх, надо переделать.
Задача: пострить алг. спец. стека со след. функциями: поместить в стек, удалить верх элемент, прверить на пустоту, прверить вкерх. значение без. удаления.
type Stack, Item' value push : Item × Stack → Stack' /*gen*/ pop : Stack → с волной Stack; /*mod*/ is_empty : Stack → Bool; /*obs*/ peek : Stack → с влной Item; /*obs*/
Аксиомы (для кждой пары obs_gen, obs_mod):
- is_empty_push
- is_empty_pop — аксиому сфрмулировать не можем
- peek_push
- peek_pop
axiom ∀ i : Item • ∀ st : Stack • is_empty(push(i, st)) &equal; false; ∀ i : Item • ∀ st : Stack • peek(push(i, st)) &equal; i;
В результате получилось две аксимы, для описания тсек этого мало. Поэтому нм необх. рассм. аксимы для случая ген_модиф.
axiom ∀ i : Item • ∀ st : Stack • pop(push(i, st)) &equal; st
Достаточно ли это для пис. стека? Наверное, нет, пэтому введём константу empty:
value empty : Stack /*gen*/
axiom is_empty(empty) &equal; true peek(empty) &equal; chaos
Этого вполне дост. для написания реализации на алг. языке.
Пстр. алг. спец. очыереди: add, remove, is_empty, peek, size
type Queue, Item; value empty : Queue; /* gen */ add : Item × Queue → Queue; /* gen */ remove : Queue → с волной Queue; /* mod */ is_empty : Queue → Bool; /* obs */ peek : Queue → с волной Item; /* obs */ size : Queue → Integer; /* obs */
Аксиомы:
- is_empty_empty
- is_empty_add
- is_empty_remove
- peek_empty
- peek_add
- peek_remove
- size_empty
- size_add
- size_remove
axiom
is_empty(empty) &equal; true;
∀ i : Item • ∀ q : Queue • is_empty(add(i, q)) &equal; false
∀ q : Queue • is_empty(remove(q)) &equal; (size(q) = 1)
pre size(q) > 0
peek(empty) &equal; chaos; ∀ i : Item • ∀ q : Queue • peek(add(i, q)) &equal; if is_empty(q) then i else peek(q) end;
size(empty) &equal; 0;
∀ i : Item • ∀ q : Queue • size(add(i, q)) &equal; size(q) + 1
∀ i : Item • ∀ q : Queue • size(remove(q)) &equal; size(q) - 1
pre size(q) > 0
Далее, исп. эту спец., предл. релиз. чередь на базе списков, и проверить непротивречивость.
type Queue : Item* value empty : Queue = <>; add(i, q) &equal; q^<i> remove(q) &equal; tl q is_empty(q) &equal; q = empty peek(q) = q(1) size(q) = len q
Доказтельство аксиомы peek(add)
peek(add(i, q)) &equal; if is_empty(q) then i else peek(q) end; (q^<i>)(1) &equal; if q = empty then i else q(1) end;
Доказтельство size(add)
size(add(i, q)) &equal; size(q) + 1 len(q ^ <i>) &equal; len(q) + 1
Формальная спецификация и верификация программ
|
|
