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

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

Перейти к: навигация, поиск

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

Текущая версия Ваш текст
Строка 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. Иногда также бывает делать полезно аксиомы для связи modificator-generator, они избыточны обычно, но наглядны.
+
Для чег нужна эта классиф? Чтобы неким разумным обр. сформ. правила, по которым форм. аксимы нашей системы. бычно, дст. сфрм. аксиому для каждй пары observer-generator, observer-modificator. Иногда также бывает делть пльзено аксимы для связи modiicator-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

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!


Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Получено с http://esyr.org/wiki/%D0%9C%D0%A4%D0%A1%D0%9F%2C_05_%D1%81%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80_%28%D0%BE%D1%82_29_%D1%81%D0%B5%D0%BD%D1%82%D1%8F%D0%B1%D1%80%D1%8F%29
Личные инструменты
Разделы