Редактирование: МФСП, 03 лекция (от 17 сентября)
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 109: | Строка 109: | ||
Практик-еор сообр: как в общем случае проверять? общего ответа нет. Какие вообще спец. включать, а какие нет? В общем случае ответа на этот вопрос нет. Практический подход такой: в наших функциях мы делаем первое грубое разделение: какие функции сзд. новые данные в нашей системе (тут мы уже разделяем целевые объекты и вспомогательные). Те операции, где мы получаем новое состояние БД, это т.н. функции-генераторы, генераторы новых значений целевого типа. Те функции, которые позволяют узнать только некоторые характеристики, это некие обсерверы, которые позволяют что-то узнать (напр, lookup). Эти функции на состояние БД не влияют. И есть ещё более тонкое деление: функция remove. Любое значение Database мною построено при помощи цепочки инсертов, и для генерации всех значений БД куьщму не нужна, а а в реальной жизни нужна и в модели должна присутствовать. Эти функции, которые несут некоторую избыточность, их называют трансформерами или модификаторами. Они меняют состояние, но они приводят к состояниям, к которым можно без них перейти. | Практик-еор сообр: как в общем случае проверять? общего ответа нет. Какие вообще спец. включать, а какие нет? В общем случае ответа на этот вопрос нет. Практический подход такой: в наших функциях мы делаем первое грубое разделение: какие функции сзд. новые данные в нашей системе (тут мы уже разделяем целевые объекты и вспомогательные). Те операции, где мы получаем новое состояние БД, это т.н. функции-генераторы, генераторы новых значений целевого типа. Те функции, которые позволяют узнать только некоторые характеристики, это некие обсерверы, которые позволяют что-то узнать (напр, lookup). Эти функции на состояние БД не влияют. И есть ещё более тонкое деление: функция remove. Любое значение Database мною построено при помощи цепочки инсертов, и для генерации всех значений БД куьщму не нужна, а а в реальной жизни нужна и в модели должна присутствовать. Эти функции, которые несут некоторую избыточность, их называют трансформерами или модификаторами. Они меняют состояние, но они приводят к состояниям, к которым можно без них перейти. | ||
- | В число аксиом системы обычно включают аксиомы, описывающие генераторы и обсерверы. А после того, как отработал генератор или трансформер, как изменилось поведение системы? А это даёт обсервера. И если для комбинаторной генерации и обс. есть опис. поведение, то это даёт эффект генератора. Т.о., мы должны согласовать с лектором, это самое абсолютное | + | В число аксиом системы обычно включают аксиомы, описывающие генераторы и обсерверы. А после того, как отработал генератор или трансформер, как изменилось поведение системы? А это даёт обсервера. И если для комбинаторной генерации и обс. есть опис. поведение, то это даёт эффект генератора. Т. о., мы должны согласовать с лектором, это самое абсолютное опис. системы, которое может быть. |
- | Теперь грустном: на | + | Теперь грустном: на экз. будет задача, на которой необходимо будет доказать правильности или неправильность уточнения. |
По поводу реальной жизни: никакие подобные системы аналитически не заказываются, на отдельные подсистемы техника доказательства используется в RAISE. Тематика становится всё более востребованной. | По поводу реальной жизни: никакие подобные системы аналитически не заказываются, на отдельные подсистемы техника доказательства используется в RAISE. Тематика становится всё более востребованной. |