МФСП, 05 семинар (от 29 сентября)

Материал из eSyr's wiki.

Текущая версия

[править] Алгебраические спецификации в RSL

Частный случай аксиоматической спецификации. Имеет следующие собенности:

1. На первом шаге формируются абстрактные типы, с которыми мы хотим работать, и целевой тип, который моделирует специфицируемую систему.
2. описываются сигнатуры функций. Только сигнатуры.
3. Формулируются аксиомы специального вида: _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.

1. Формулировка типов. Выбор целевого типа
2. Написание сигнатур. (Как в ООП: выбираем классы, и пишем методы)
3. Формулируем аксиомы, связывающие функции, используя алгебраический подход. В результате получается алгебраическая спецификация.
4. После чего итерационно идёт пошаговая реализация.
   • Уточнить тип
   • Спецификация функции
   • При этом необходимо соблюдать непротиворечивость исходных аксиом алгебраической спецификации.

Прверять каждую аксиому и доказывать руками тяжело, есть автоматизированные средства, но на практикуме оно не потребуется.

Пример (из примера пр БД): допустим, мы на некоем шаге реализации решили, что

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