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

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

(Различия между версиями)
Перейти к: навигация, поиск
м
Строка 1: Строка 1:
-
лгебраические спецификации в rsl.
+
== Алгебраические спецификации в RSL ==
Чстный случай аксиом. спецификации. Имеет след. собенности:
Чстный случай аксиом. спецификации. Имеет след. собенности:
Строка 5: Строка 5:
# На первом шаге фрм. абстрактные типы, с ктрым мы хтим рабтть, и целевй тип, кторый мделир. специфиц. систему.
# На первом шаге фрм. абстрактные типы, с ктрым мы хтим рабтть, и целевй тип, кторый мделир. специфиц. систему.
# писываются сигнатуры функций. Тольк сигнтуры.
# писываются сигнатуры функций. Тольк сигнтуры.
-
# Фрмулируются аксиомы специальнго вида: _i(f_i(x), ..., f_n(x)) == expr. Это требуется для выявления свйств, не пр. их.
+
# Фрмулируются аксиомы специальнго вида: _i(f_i(x), ..., f_n(x)) &equal; expr. Это требуется для выявления свйств, не пр. их.
Пример:
Пример:
Строка 33: Строка 33:
Далее выпис. все аксимы, используя в кач. арг. раз. переменные, кторые потм змык. квантором всеобщности. Правя чсть аксиом пишется сотв. семнтике. Если функ. част. спец., т небх. опр. предусловия.
Далее выпис. все аксимы, используя в кач. арг. раз. переменные, кторые потм змык. квантором всеобщности. Правя чсть аксиом пишется сотв. семнтике. Если функ. част. спец., т небх. опр. предусловия.
'''axiom'''
'''axiom'''
-
∀ k : Key ˙ defined(k, empty) == false
+
∀ k : Key • defined(k, empty) &equal; 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 • ∀ 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)) == (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)) == if k_1 = k_2 then r else lookup(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)
'''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)
+
∀ 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)
'''pre''' (k_1 ≠ k_2) ∧ defined(k_1, db)
Строка 45: Строка 45:
Потому что этот пдх из функ. пргр. Мы этими ксимми задаём алгебр. отношения.
Потому что этот пдх из функ. пргр. Мы этими ксимми задаём алгебр. отношения.
-
Сам прцесс пректирвния программы в технологии RAISE.
+
Сам процесс проектирования программы в технологии RAISE.
-
# Фрмулировка типов. Выбр целевого типа
+
# Формулировка типов. Выбор целевого типа
# Написание сигнатур. (Как в ООП: выбираем классы, и пишем методы)
# Написание сигнатур. (Как в ООП: выбираем классы, и пишем методы)
-
# Фрмулируем акиомы, связ. функции, исп. алг. пдхд. В рез-те получается алг. спецификция.
+
# Формулируем аксиомы, связ. функции, исп. алг. подход. В рез-те получается алг. спецификация.
-
# Псле чег итерцинно идёт пшаговая реализация.
+
# После чего итерационно идёт пошаговая реализация.
#* Уточнить тип
#* Уточнить тип
-
#* Спецификция функции
+
#* Спецификация функции
-
#* При этом небходимо соблюдать непротиврчеивость исх. аксиом алг. спецификации.
+
#* При этом необходимо соблюдать непротиворечивость исх. аксиом алг. спецификации.
Прверять каждую акс. и дказывать руками тяжело, есть авт. средства, но на практикуме оно не потребуется.
Прверять каждую акс. и дказывать руками тяжело, есть авт. средства, но на практикуме оно не потребуется.
Строка 62: Строка 62:
empty : Database = {}
empty : Database = {}
-
defined(k,db) = ∃r : Record ˙ (k, r) ∈ db
+
defined(k,db) = ∃r : Record • (k, r) ∈ db
Теперь прверим, что специф. не пртивор. аксиоме:
Теперь прверим, что специф. не пртивор. аксиоме:
[define_empty]
[define_empty]
-
∀ k : Key ˙ defined(k, empty) == false
+
∀ k : Key • defined(k, empty) &equal; false
-
&fora;; k : Key ˙ ∃r : Record ˙ (k, r) ∈ {} == false
+
&fora;; k : Key • ∃r : Record • (k, r) ∈ {} &equal; false
-
У нас матлг был, метды резолюции знаем, всё очевидно. Левая часть тжд. равна false, false==false, аксиома выполняется.
+
У нас матлг был, метды резолюции знаем, всё очевидно. Левая часть тжд. равна false, false&equal;false, аксиома выполняется.
На практикуме форм. док. треб. не будет, но если бн. противоречие, то плх, надо переделать.
На практикуме форм. док. треб. не будет, но если бн. противоречие, то плх, надо переделать.
Строка 90: Строка 90:
'''axiom'''
'''axiom'''
-
∀ i : Item ˙ ∀ st : Stack ˙ is_empty(push(i, st)) == false;
+
∀ i : Item • ∀ st : Stack • is_empty(push(i, st)) &equal; false;
-
∀ i : Item ˙ ∀ st : Stack ˙ peek(push(i, st)) == i;
+
∀ i : Item • ∀ st : Stack • peek(push(i, st)) &equal; i;
В результате получилось две аксимы, для описания тсек этого мало. Поэтому нм необх. рассм. аксимы для случая ген_модиф.
В результате получилось две аксимы, для описания тсек этого мало. Поэтому нм необх. рассм. аксимы для случая ген_модиф.
'''axiom'''
'''axiom'''
-
∀ i : Item ˙ ∀ st : Stack ˙ pop(push(i, st)) == st
+
∀ i : Item • ∀ st : Stack • pop(push(i, st)) &equal; st
Достаточно ли это для пис. стека? Наверное, нет, пэтому введём константу empty:
Достаточно ли это для пис. стека? Наверное, нет, пэтому введём константу empty:
Строка 102: Строка 102:
'''axiom'''
'''axiom'''
-
is_empty(empty) == true
+
is_empty(empty) &equal; true
-
peek(empty) == chaos
+
peek(empty) &equal; chaos
Этого вполне дост. для написания реализации на алг. языке.
Этого вполне дост. для написания реализации на алг. языке.
Строка 131: Строка 131:
'''axiom'''
'''axiom'''
-
is_empty(empty) == true;
+
is_empty(empty) &equal; true;
-
∀ i : Item ˙ ∀ q : Queue ˙ is_empty(add(i, q)) == false
+
∀ i : Item • ∀ q : Queue • is_empty(add(i, q)) &equal; false
-
∀ q : Queue ˙ is_empty(remove(q)) == (size(q) = 1)
+
∀ q : Queue • is_empty(remove(q)) &equal; (size(q) = 1)
'''pre''' size(q) > 0
'''pre''' size(q) > 0
-
peek(empty) == chaos;
+
peek(empty) &equal; chaos;
-
∀ i : Item ˙ ∀ q : Queue ˙ peek(add(i, q)) == if is_empty(q) then i else peek(q) end;
+
∀ i : Item • ∀ q : Queue • peek(add(i, q)) &equal; if is_empty(q) then i else peek(q) end;
-
size(empty) == 0;
+
size(empty) &equal; 0;
-
∀ i : Item ˙ ∀ q : Queue ˙ size(add(i, q)) == size(q) + 1
+
∀ i : Item • ∀ q : Queue • size(add(i, q)) &equal; size(q) + 1
-
∀ i : Item ˙ ∀ q : Queue ˙ size(remove(q)) == size(q) - 1
+
∀ i : Item • ∀ q : Queue • size(remove(q)) &equal; size(q) - 1
'''pre''' size(q) > 0
'''pre''' size(q) > 0
Строка 150: Строка 150:
'''value'''
'''value'''
empty : Queue = <>;
empty : Queue = <>;
-
add(i, q) == q^&lt;i>
+
add(i, q) &equal; q^&lt;i>
-
remove(q) == tl q
+
remove(q) &equal; tl q
-
is_empty(q) == q = empty
+
is_empty(q) &equal; q = empty
peek(q) = q(1)
peek(q) = q(1)
size(q) = len q
size(q) = len q
Доказтельство аксиомы peek(add)
Доказтельство аксиомы peek(add)
-
peek(add(i, q)) == if is_empty(q) then i else peek(q) end;
+
peek(add(i, q)) &equal; if is_empty(q) then i else peek(q) end;
-
(q^&lt;i>)(1) == if q = empty then i else q(1) end;
+
(q^&lt;i>)(1) &equal; if q = empty then i else q(1) end;
Доказтельство size(add)
Доказтельство size(add)
-
size(add(i, q)) == size(q) + 1
+
size(add(i, q)) &equal; size(q) + 1
-
len(q ^ &lt;i>) == len(q) + 1
+
len(q ^ &lt;i>) &equal; len(q) + 1
{{МФСП}}
{{МФСП}}
{{Lection-stub}}
{{Lection-stub}}

Версия 15:37, 4 октября 2008

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

  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


Формальная спецификация и верификация программ


Лекции

01 02 03 04 05 06 07 08 09 10 11 12 13 14


Календарь

Сентябрь
03 10 17 24
Октябрь
01 08 15 22 29
Ноябрь
12 19 26
Декабрь
03 17
Семинары

01 02 03 04 05 06


Календарь

Сентябрь
01 08 15 22 29
Октябрь
06

Оформление задач|Проведение экзамена


Эта статья является конспектом лекции.

Эта статья ещё не вычитана. Пожалуйста, вычитайте её и исправьте ошибки, если они есть.
Личные инструменты
Разделы