OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Суббота, 22 Июль, 2017 11:42

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




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

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

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

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

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


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

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


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

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

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

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

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

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


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

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

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


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

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


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

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


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

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