OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Воскресенье, 24 Сентябрь, 2017 18:48

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 7 ] 
Автор Сообщение
 Заголовок сообщения: Типы инвариантов
СообщениеДобавлено: Четверг, 25 Май, 2017 13:34 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 562
Откуда: Казань
Многие наверно слышали про инвариант цикла. Кое-кто может быть слышал про инвариант класса в языке Eiffel. Но также выделяют еще инвариант рекурсии, инвариант итератора и инвариант данных.

Кто как считает необходимы ли все эти инварианты?
Например, зачем нужен инвариант рекурсии, когда у рекурсивной функции может быть предусловие и постусловие? (В принципе для рекурсии была бы полезна ограничивающая функция, которая бы показывала, что рекурсия завершается, а не "зацикливается" и не вылетает при исчерпании стека.)

Нужно ли отдельно выделять инвариант данных или достаточно того, что описаны все постусловия всех функций, которые работают с данными и известно что может быть с данными?

И если кто-то знает где можно почитать не про инвариант цикла, а про другие инварианты, то был бы благодарен за ссылку.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Типы инвариантов
СообщениеДобавлено: Четверг, 25 Май, 2017 14:11 
Аватара пользователя

Зарегистрирован: Воскресенье, 12 Апрель, 2015 18:12
Сообщения: 981
Откуда: СССР v2.0 rc 1
Любая новая деталь автомата снижает надёжность автомата.
Имхо, достаточно ассерта на входе и выходе. Это отловит 95% недопустимых состояний.
Я против избыточных сущностей.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Типы инвариантов
СообщениеДобавлено: Четверг, 25 Май, 2017 16:42 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 458
Откуда: Киев
Rifat писал(а):
Многие наверно слышали про инвариант цикла. Кое-кто может быть слышал про инвариант класса в языке Eiffel. Но также выделяют еще инвариант рекурсии, инвариант итератора и инвариант данных.
Инварианты класса и итератора - это, пожалуй, частные случаи инварианта данных. Инвариант данных - это часть инварианта всех процедур, которые используют эти данные.

Инвариант рекурсивной или обычной процедуры - это набор условий, совпадающих в пред- и в пост- условиях. Таким образом, всё может быть сведено к пред- и пост- условиям, а выделяют эти понятия отдельно, чтобы не повторяться из раза в раз. Если в задаче много таких повторов, то и понятия становятся нужны.

Часть пред- и пост- условий могут быть выражены через ASSERT, тем не менее, это далеко не всегда оправдано. Часть условий должны, во-первых, служить документацией, а , во-вторых, быть проверены на этапе трансляции, если это возможно. И только самые легковестные проверки можно вынести на этап исполнения.

Цитата:
Кто как считает необходимы ли все эти инварианты?

Считаю, что они нужны в понятиях языка, чтобы иметь возможность доказывать корректность программ автоматическими средствами, не прибегая к трюкам, наподобии спец-комментариев. Но подойти к внедрению нужно осторожно, потому что легко доулучшаться до невозможности легко программировать.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Типы инвариантов
СообщениеДобавлено: Четверг, 25 Май, 2017 16:45 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 458
Откуда: Киев
prospero78 писал(а):
Любая новая деталь автомата снижает надёжность автомата.
Имхо, достаточно ассерта на входе и выходе. Это отловит 95% недопустимых состояний.
Я против избыточных сущностей.

Указанные средства - это не столько новые детали автомата, сколько процедуры здачи-приёмки. АК много где выпускается, но оригинальный ценится особо за контроль качества.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Типы инвариантов
СообщениеДобавлено: Четверг, 27 Июль, 2017 20:32 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 149
Rifat писал(а):
И если кто-то знает где можно почитать не про инвариант цикла, а про другие инварианты, то был бы благодарен за ссылку.

Единой теории не укажу (да и вряд ли такова существует). Ниже эмпирические наблюдения (впрочем, в сопутствующих материалах полно теоретических изложений разного толка).
Rifat писал(а):
Например, зачем нужен инвариант рекурсии, когда у рекурсивной функции может быть предусловие и постусловие? (В принципе для рекурсии была бы полезна ограничивающая функция, которая бы показывала, что рекурсия завершается, а не "зацикливается" и не вылетает при исчерпании стека.)

Ограничение рекурсии (цикла) необходимая вещь. В качестве примера -- современный "мейнстрим" в области верификации --
проект Dafny:
https://www.microsoft.com/en-us/researc ... rrectness/

проект F-Star:
https://fstar-lang.org/

где имеется директива "decreases" (в мощной системе вывода типа как в F-Star условие рекурсии в ряде случаев определяется автоматом, также как и остальные ограничения типа).

Можно обратить внимание, что в Dafny нет инварианта для класса, и используются контракты состояния объекта (косвенно через функции/методы) для каждого необходимого метода класса (как универсальный способ, поскольку состояние объекта изменяется). В F-Star имеются ограничения для типов данных (в общем-то, здесь явно декларируются "зависимые типы"), но нет инвариантов для операторов цикла (да и не нужны они). Техники F-Star мощнее, и требуется явное именование объектов для контракта (собственно, там именно ограничения типов). К примеру, "леммы" там указывают на качество конкретных объектов.

У F-Star имеются неплохие расширения, как "реляционные контракты":
https://www.microsoft.com/en-us/researc ... 02/rrf.pdf

где в дополнение к "классическим" пред/постусловиям используется отношение между результатами двух вычислений выражения. Это техника в т.ч. и для анализа условно "неограниченной" рекурсии.

Следует отметить, что контракты операций могут выражать не только пред/постусловия как таковые (т.е. инвариант "прикладного", "предметного" состояния), но и качественные свойства. В том же F-Star таковым активно занимаются, или вот примеры "аксиом" здесь (что есть в т.ч. и подсказки для компилятора для правильных или эффективных реализаций/оптимизаций):
http://felix-lang.org/share/src/web/tut ... sm_03.fdoc


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Типы инвариантов
СообщениеДобавлено: Четверг, 27 Июль, 2017 20:40 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 149
Инварианты, о которых речь здесь выше во всей теме, условно можно отнести к "зависимым типам" ("dependent types" или "liquid types" и прочие вариации). Часто в ООП-среде это дело обзывается как программирование (или моделирование) "по контрактам" и т.п. В общем, термины всякие "резиновые", и речь не о теоретических изысках. Прежде всего, имеется ввиду контракты, зависимые от данных или состояния. Однако, есть пласт инвариантов, где эта зависимость от состояния косвенная или скрытая.

Первый такой слой в программистском жаргоне -- "typestate". Упрощенно, для типа с набором операций важен порядок их применения, и этот порядок задаётся как интерфейс типа. К примеру, в языке Rust попытка реализации typestate провалилась:
http://pcwalton.github.io/blog/2012/12/ ... e-is-dead/

Есть проект Vault от MS, расширение для С:
https://www.microsoft.com/en-us/researc ... pldi01.pdf

где объект представляется виртуальным автоматом (попутно в Vault решается и задача управления памятью).

В принципе, можно "выкручиваться" косвенно, как, например, в Dafny имеются ghost-переменные, вводимые лишь для верификации (т.е. "физически" не включаются в тип), и с их помощью в предусловии метода можно контролировать допустимость исполнения. Тем не менее, порядок операций "клиент" типа всё равно вынужден как-то понимать. К тому же механизмы аля ghost-переменных -- сугубо внутренняя реализация типа (для всяких целей, в т.ч. и верификации, тестирования и пр.) и не должны быть в интерфейсе.

Ещё пример (на базе языка Lustre из платформы Esterel, разбираемой здесь на форуме по соседству):
https://pdfs.semanticscholar.org/f570/9 ... 83acca.pdf

где контракт м.б. определен и автоматически как часть вывода типа.


Контракты "typestate" выше -- односторонние, или контракты ресурса. Для двусторонних и более возникает новый пласт -- "session types". Здесь собраны не мало тематических ресурсов:
http://simonjf.com/2016/05/28/session-t ... tions.html

По ссылке выше основные решения на базе пи-исчисления процессов. Поэтому там явный "message passing". Контракты -- через системы типов в языке, формулы сессий или спец-языки как Scribble. Последний набирает популярность, имеются всякие расширения аля Parameterised Scribble:
https://groups.inf.ed.ac.uk/abcd/meetin ... las-ng.pdf

Или ещё параметры-атрибуты (для анализа времени и др.):
http://mrg.doc.ic.ac.uk/publications/ti ... /paper.pdf

Кстати, именно в рамках контрактов "type state" и "session types" уже проблематично игнорировать основную пакость для верификаторов. Грубо говоря, анализатор может отслеживать переменную и следить за семантикой вычислений, но когда переменная "улетает", напр., "помещается" в контейнер -- всё, приехали. Когда как в сессиях "разрыв" типа, фактически, неизбежен, или должен быть предусмотрен. Для примера -- реализация "сессионных типов" для Java:
https://www.doc.ic.ac.uk/~rhu/sessionj/ ... safe10.pdf

где на борту run-time механизмы ("typecase" и др.). Или же см. примеры для OCaml, Rust, Scala и др. (в статье-сборнике по сессионным типам по ссылке выше), где "выкручиваются" через статические "хаки" для своих систем типов в языке.

В общем, проблема верификации далеко не только в том, где задавать контракты (в комментариях или нет, согласно соседней теме форума про "виртуальный текст"). И конечно же, жизнь проще, если для всего иметь один язык (как Lustre-like, где программа (верифицируемая) есть и модель взаимодействия процессов, в т.ч. и как контракт для их возможного "разделения").


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Типы инвариантов
СообщениеДобавлено: Воскресенье, 30 Июль, 2017 14:48 

Зарегистрирован: Вторник, 30 Июнь, 2009 14:58
Сообщения: 1362
Rifat, не стоит искать в программировании каких-то особых "инвариантов".

Инвариант - это уравнение, которое всегда выполняется.
С их помощью мы фиксируем свои предположения насчет некоторого объекта (системы).
Совокупность инвариантов по сути определяет идеальную модель системы.
Это позволяет нам:
1. Делать проверки - что система ведет себя так, как мы предполагаем.
2. Использовать инварианты как аксиомы в своих рассуждениях.


Цитата:
И если кто-то знает где можно почитать не про инвариант цикла, а про другие инварианты, то был бы благодарен за ссылку.

Попробуйте порассуждать самостоятельно.
Возьмите какой-нибудь простой объект. Например, кирпич.
Кирпич - это система из частиц (углубляться в сущность самих частиц не нужно)
Что делает кирпич кирпичом? Подумайте над этим.
Кирпич вообще говоря существует только в нашем воображении. Удивительно то, что большинство людей сходятся во мнении, что некоторый объект является кирпичом.
Как же так выходит?

Попробуйте зафиксировать ваше представление о кирпиче формально в виде уравнений.
У вас есть положения частиц в трехмерном пространстве. Их скорости и т.д.
Другими словами у вас есть переменные, которые можно связать уравнениями, чтобы получить кирпич.
Записав некоторый набор уравнений вы получите модель системы "кирпич".
Модель может быть очень грубой, но при этом достаточной, чтобы большинство людей согласилось, что это описание кирпича.

Так вот в программировании ровно то же самое. Вы создаете систему. У вас есть некоторая модель будущей системы в голове. Фиксируете эту модель в виде уравнений, и втыкаете в код проверки, что уравнения выполняются.
Цикл - это просто часть системы. Никаких особенных инвариантов там нет.
Да и вообще не стоит искать в слове "инвариант" скрытых смыслов. Их там нет.
Инварианты - это просто способ (один из...) формализации наших представлений о некотором явлении/объекте/системе.


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 7 ] 

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 1


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2005-2017, участники конференции «OberonCore», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Без разрешения участников и ссылки на конференцию «OberonCore» любое воспроизведение и/или копирование высказываний полностью и/или по частям запрещено.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB