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

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

(Различия между версиями)
Перейти к: навигация, поиск
 
Строка 1: Строка 1:
== Алгебраические спецификации в RSL ==
== Алгебраические спецификации в RSL ==
-
Чстный случай аксиом. спецификации. Имеет след. собенности:
+
Частный случай аксиоматической спецификации. Имеет следующие собенности:
-
# На первом шаге фрм. абстрактные типы, с ктрым мы хтим рабтть, и целевй тип, кторый мделир. специфиц. систему.
+
# На первом шаге формируются абстрактные типы, с которыми мы хотим работать, и целевой тип, который моделирует специфицируемую систему.
-
# писываются сигнатуры функций. Тольк сигнтуры.
+
# описываются сигнатуры функций. Только сигнатуры.
-
# Фрмулируются аксиомы специальнго вида: _i(f_i(x), ..., f_n(x)) &equal; expr. Это требуется для выявления свйств, не пр. их.
+
# Формулируются аксиомы специального вида: _i(f_i(x), ..., f_n(x)) &equal; expr. Это требуется для выявления свойств, не пр. их.
Пример:
Пример:
Строка 19: Строка 19:
Мы прошли первых два этапа.
Мы прошли первых два этапа.
-
Для удобства принято выд. дв типа перций: генератор (операция, прим. ктрой позв. плучить любое знач. целевого типа). Тут их два: insert, empty. Генертры и среди перндов имеет целевй тип, и знач цеевой тип. Операции, к-рые называются observer, не меняют целевй тип, а возвр. инф., связнную с ним. И модификторы. Частный случай генератора, но с пмощью них нельзя плучить любое знач. целевого типа. Но при этм они меняют цел. тип.
+
Для удобства принято выделять два типа оперций: генератор (операция, применение которой позволяет получить любое значение целевого типа). Тут их два: insert, empty. Генератор среди операндов имеет целевой тип, и значение целевой тип. Операции, которые называются observer, не меняют целевой тип, а возвращают информацию, связанную с ним. И модификаторы — частный случай генератора, но с помощью них нельзя получить любое значение целевого типа. Но при этом они меняют целевой тип.
-
Для чег нужна эта классиф? Чтобы неким разумным обр. сформ. правила, по которым форм. аксимы нашей системы. бычно, дст. сфрм. аксиому для каждй пары observer-generator, observer-modificator. Иногда также бывает делть пльзено аксимы для связи modiicator-generator, они избыточны бычн, но нглядны.
+
Для чего нужна эта классификация? Чтобы неким разумным образом сформулировать правила, по которым формируются аксимы нашей системы. Обычно, достаточно сформулировать аксиому для каждой пары observer-generator, observer-modificator. Иногда также бывает делать полезно аксиомы для связи modificator-generator, они избыточны обычно, но наглядны.
-
Теперь будем выпис. аксиомы, удовл. нашей операции:
+
Теперь будем выписывать аксиомы, удовлетворяющие нашей операции:
* defined_empty
* defined_empty
* defined_insert
* defined_insert
Строка 31: Строка 31:
lookup_empty — не имеет смысла, опущена.
lookup_empty — не имеет смысла, опущена.
-
Далее выпис. все аксимы, используя в кач. арг. раз. переменные, кторые потм змык. квантором всеобщности. Правя чсть аксиом пишется сотв. семнтике. Если функ. част. спец., т небх. опр. предусловия.
+
Далее выписываем все аксиомы, используя в качестве аргументов различные переменные, которые потом замыкаются квантором всеобщности. Правая часть аксиом пишется соответственно семантике. Если функция частично специфицирована, то необходимо определить предусловия.
'''axiom'''
'''axiom'''
∀ k : Key • defined(k, empty) &equal; false
∀ k : Key • defined(k, empty) &equal; false
Строка 41: Строка 41:
'''pre''' (k_1 ≠ k_2) ∧ defined(k_1, db)
'''pre''' (k_1 ≠ k_2) ∧ defined(k_1, db)
-
Почему эт нз. алг. спец?
+
Почему эт называется алгебраической спецификацией?
-
Потому что этот пдх из функ. пргр. Мы этими ксимми задаём алгебр. отношения.
+
Потому что этот подход из функционального программирования. Мы этими аксиомами задаём алгебраические отношения.
Сам процесс проектирования программы в технологии RAISE.
Сам процесс проектирования программы в технологии RAISE.
# Формулировка типов. Выбор целевого типа
# Формулировка типов. Выбор целевого типа
# Написание сигнатур. (Как в ООП: выбираем классы, и пишем методы)
# Написание сигнатур. (Как в ООП: выбираем классы, и пишем методы)
-
# Формулируем аксиомы, связ. функции, исп. алг. подход. В рез-те получается алг. спецификация.
+
# Формулируем аксиомы, связывающие функции, используя алгебраический подход. В результате получается алгебраическая спецификация.
# После чего итерационно идёт пошаговая реализация.
# После чего итерационно идёт пошаговая реализация.
#* Уточнить тип
#* Уточнить тип
#* Спецификация функции
#* Спецификация функции
-
#* При этом необходимо соблюдать непротиворечивость исх. аксиом алг. спецификации.
+
#* При этом необходимо соблюдать непротиворечивость исходных аксиом алгебраической спецификации.
-
Прверять каждую акс. и дказывать руками тяжело, есть авт. средства, но на практикуме оно не потребуется.
+
Прверять каждую аксиому и доказывать руками тяжело, есть автоматизированные средства, но на практикуме оно не потребуется.
-
Пример (из примера пр БД): допустим, мы на некем шаге релиз. решили, что
+
Пример (из примера пр БД): допустим, мы на некоем шаге реализации решили, что
'''type'''
'''type'''
Database = Key × Record-set
Database = Key × Record-set
Строка 64: Строка 64:
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) &equal; false
∀ k : Key • defined(k, empty) &equal; false
&fora;; k : Key • ∃r : Record • (k, r) ∈ {} &equal; false
&fora;; k : Key • ∃r : Record • (k, r) ∈ {} &equal; false
-
У нас матлг был, метды резолюции знаем, всё очевидно. Левая часть тжд. равна false, false&equal;false, аксиома выполняется.
+
У нас матлог был, методы резолюции знаем, всё очевидно. Левая часть тождественно равна false, false&equal;false, аксиома выполняется.
-
На практикуме форм. док. треб. не будет, но если бн. противоречие, то плх, надо переделать.
+
На практикуме формулировать доказательства требоваться не будет, но если обнаружено противоречие, то плохо, надо переделать.
-
Задача: пострить алг. спец. стека со след. функциями: поместить в стек, удалить верх элемент, прверить на пустоту, прверить вкерх. значение без. удаления.
+
Задача: построить алгебраическую спецификацию стека со следующими функциями: поместить в стек, удалить верхний элемент, проверить на пустоту, проверить верхнее значение без удаления.
'''type'''
'''type'''
Строка 83: Строка 83:
peek : Stack → с влной Item; /*obs*/
peek : Stack → с влной Item; /*obs*/
-
Аксиомы (для кждой пары obs_gen, obs_mod):
+
Аксиомы (для каждой пары obs_gen, obs_mod):
* is_empty_push
* is_empty_push
-
* is_empty_pop — аксиому сфрмулировать не можем
+
* is_empty_pop — аксиому сформулировать не можем
* peek_push
* peek_push
* peek_pop
* peek_pop
Строка 93: Строка 93:
∀ i : Item • ∀ st : Stack • peek(push(i, st)) &equal; i;
∀ i : Item • ∀ st : Stack • peek(push(i, st)) &equal; i;
-
В результате получилось две аксимы, для описания тсек этого мало. Поэтому нм необх. рассм. аксимы для случая ген_модиф.
+
В результате получилось две аксиомы, для описания стека этого мало. Поэтому нам необходимо рассмотреть аксиомы для случая ген_модиф.
'''axiom'''
'''axiom'''
∀ i : Item • ∀ st : Stack • pop(push(i, st)) &equal; st
∀ i : Item • ∀ st : Stack • pop(push(i, st)) &equal; st
-
Достаточно ли это для пис. стека? Наверное, нет, пэтому введём константу empty:
+
Достаточно ли это для описания стека? Наверное, нет, поэтому введём константу empty:
'''value'''
'''value'''
empty : Stack /*gen*/
empty : Stack /*gen*/
Строка 105: Строка 105:
peek(empty) &equal; chaos
peek(empty) &equal; chaos
-
Этого вполне дост. для написания реализации на алг. языке.
+
Этого вполне достаточно для написания реализации на алгоритмическом языке.
-
Пстр. алг. спец. очыереди: add, remove, is_empty, peek, size
+
Построить алгебраическую спецификацию очереди: add, remove, is_empty, peek, size
'''type'''
'''type'''
Строка 144: Строка 144:
'''pre''' size(q) > 0
'''pre''' size(q) > 0
-
Далее, исп. эту спец., предл. релиз. чередь на базе списков, и проверить непротивречивость.
+
Далее, использовать эту спецификацию, предложено реализовать очередь на базе списков, и проверить непротивречивость.
'''type'''
'''type'''
Строка 156: Строка 156:
size(q) = len q
size(q) = len q
-
Доказтельство аксиомы peek(add)
+
Доказательство аксиомы peek(add)
peek(add(i, q)) &equal; 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^<i>)(1) &equal; if q = empty then i else q(1) end;
(q^<i>)(1) &equal; if q = empty then i else q(1) end;
-
Доказтельство size(add)
+
Доказательство size(add)
size(add(i, q)) &equal; size(q) + 1
size(add(i, q)) &equal; size(q) + 1
len(q ^ <i>) &equal; len(q) + 1
len(q ^ <i>) &equal; len(q) + 1

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

[править] Алгебраические спецификации в 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


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


Лекции

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

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


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

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