МФСП, 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. Иногда также бывает делать полезно аксиомы для связи modificator-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
Формальная спецификация и верификация программ
|
|
