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

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

лгебраические спецификации в rsl.

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

1. На первом шаге фрм. абстрактные типы, с ктрым мы хтим рабтть, и целевй тип, кторый мделир. специфиц. систему.
2. писываются сигнатуры функций. Тольк сигнтуры.
3. Фрмулируются аксиомы специальнго вида: _i(f_i(x), ..., f_n(x)) == 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) == false
  ∀ k_1, k_2 : Key ˙ ∀ r : Record ˙ ∀ db : Database ˙ defined(k_1, insert(k_2, r, db)) == (k_1 = k_2) ∨ defined(k_1, db) 
  ∀ k_1, k_2 : Key ˙ ∀ db : Database ˙ defined(k_1, remove(k_2, db)) == (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)) == 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)) == 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) == false
  &fora;; k : Key ˙ ∃r : Record ˙ (k, r) ∈ {} == false

У нас матлг был, метды резолюции знаем, всё очевидно. Левая часть тжд. равна false, false==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)) == false;
  ∀ i : Item ˙ ∀ st : Stack ˙ peek(push(i, st)) == i;

В результате получилось две аксимы, для описания тсек этого мало. Поэтому нм необх. рассм. аксимы для случая ген_модиф.

axiom
  ∀ i : Item ˙ ∀ st : Stack ˙ pop(push(i, st)) == st

Достаточно ли это для пис. стека? Наверное, нет, пэтому введём константу empty:

value
  empty : Stack /*gen*/

axiom
  is_empty(empty) == true
  peek(empty) == 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) == true;
  ∀ i : Item ˙ ∀ q : Queue ˙ is_empty(add(i, q)) == false
  ∀ q : Queue ˙ is_empty(remove(q)) == (size(q) = 1)
    pre size(q) > 0

  peek(empty) == chaos;
  ∀ i : Item ˙ ∀ q : Queue ˙ peek(add(i, q)) == if is_empty(q) then i else peek(q) end;

  size(empty) == 0;
  ∀ i : Item ˙ ∀ q : Queue ˙ size(add(i, q)) == size(q) + 1
  ∀ i : Item ˙ ∀ q : Queue ˙ size(remove(q)) == size(q) - 1
    pre size(q) > 0

Далее, исп. эту спец., предл. релиз. чередь на базе списков, и проверить непротивречивость.

type
  Queue : Item*
value
  empty : Queue = <>;
  add(i, q) == q^<i>
  remove(q) == tl q
  is_empty(q) == q = empty
  peek(q) = q(1)
  size(q) = len q

Доказтельство аксиомы peek(add)

peek(add(i, q)) == if is_empty(q) then i else peek(q) end;
(q^<i>)(1) == if q = empty then i else q(1) end;

Доказтельство size(add)

size(add(i, q)) == size(q) + 1
len(q ^ <i>) == len(q) + 1