OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Вторник, 19 Март, 2024 07:05

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




Начать новую тему Ответить на тему  [ Сообщений: 23 ]  На страницу 1, 2  След.
Автор Сообщение
 Заголовок сообщения: Виртуальный текст
СообщениеДобавлено: Вторник, 25 Июль, 2017 16:54 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 987
Откуда: Казань
Несколько лет назад было обсуждение:
AVC писал(а):
Alexey Veselovsky писал(а):
Ну, на западе для подобного в моде Ада, и построение инструментария для верификации ПО. Т.е. пишешь само ПО, пишешь к нему верификационный инструментарий. Отдаешь и то и другое заказчику в исходниках. Также там моден SPARK (http://en.wikipedia.org/wiki/SPARK_(pro ... g_language)), по сути это подмножество Ады + средства верификации.
Спасибо за ссылку на SPARK.
Интересно также насчёт "самописного" верификационного инструментария (хотя не вполне ясно, что он из себя представляет).

Как я понимаю, по поводу "самописного" верификационного инструментария имеется в виде механизм виртуального текста из языка Anna для Ada или похожий механизм абстрактных функций из SPARK.
Суть в том, что можно описывать свой функции, которые нужны только для верификации программы (для формальной или же run-time) и не требуются для работы самой программы. Например, в программе, которая работает с сбалансированным AVL деревом можно написать функцию, которая проверяет сбалансированность дерева. И использовать эти функции в утверждениях в различных местах программы. То есть, если, например, Unit Test рассматривают функции программы как черные ящики и проверяют их на конкретных входных значениях и проверяется совпадают ли выходные значения. То виртуальный текст из Ada помогает проверять свойства программы, например, что дерево сбалансировано, массив отсортирован и т.д.. Таким образом получается self-checking программа. Это довольно таки интересная идея, похоже она получила развитие только в области языка программирования Ada.
Как думаете, будет ли полезен подобный механизм виртуального текста для языка Оберон?


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Виртуальный текст
СообщениеДобавлено: Вторник, 25 Июль, 2017 18:12 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1447
Откуда: Киев
Дадите пример?


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Виртуальный текст
СообщениеДобавлено: Среда, 26 Июль, 2017 10:29 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 9459
Откуда: Россия, Орёл
Мы у себя в АСУТП что-то типа простого Self-Checking-а тоже применяем.
Каждый Оберон-мессидж имеет процедуру Check, состояние любого объекта тоже имеет процедуру валидации - и эти валидации выполняются как при прохождении мессиджей, так и при установке нового состояния объекта после такта работы логики.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Виртуальный текст
СообщениеДобавлено: Среда, 26 Июль, 2017 10:59 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 987
Откуда: Казань
Примеры кода на ANNA (ANNotations for Ada):
Вложение:
anna1.png
anna1.png [ 46.16 КБ | Просмотров: 11423 ]

Вложение:
Anna3.png
Anna3.png [ 87.22 КБ | Просмотров: 11423 ]


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Виртуальный текст
СообщениеДобавлено: Среда, 26 Июль, 2017 11:27 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1447
Откуда: Киев
Теперь ясно. Да, нужно, но не для Oberon, потому что, по-хорошему, такие вещи должны быть учтены в языке сразу, а это уже не Oberon.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Виртуальный текст
СообщениеДобавлено: Среда, 26 Июль, 2017 12:14 
Аватара пользователя

Зарегистрирован: Воскресенье, 12 Апрель, 2015 18:12
Сообщения: 1134
Откуда: СССР v2.0 rc 1
Рифат ,мы всё ещё возвращаемся к проблеме "верификация верификатора". В Обероне есть пред- и пост- условия + строгая типизация + проверка границ структур данных этапа исполнения + сборщик мусора.
По сути, 90% всех ошибок -- это последние две килл-фичи Оберона.

Что касается верификации, тут вспоминаем теорему о полноте и тут же грустнеем.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Виртуальный текст
СообщениеДобавлено: Среда, 26 Июль, 2017 13:28 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 987
Откуда: Казань
В книге "Programming with Specifications" David Luckham-а есть следующая строчка:
Цитата:
The idea of virtual text is very simple: "write a program to describe a program, but keep the two programs separate." Virtual text is the separating feature.

и еще есть следующие интересные предложения:
Цитата:
Another observation is that most informal comments can be expressed in a formal language similar to the programming language itself. It is called formal because precise rules define its syntax and semantics. Comments written in a formal language are called formal comments. They can be parsed, checked for semantic validity, and translated into an executable form by techniques similar to those used in compiling a program.


Насколько я понимаю, ANNA - это как бы препроцессор над Ada. Виртуальный текст находится в комментариях относительно исходной Ada программы. Но препроцессор ANNA распознает виртуальный текст (обычные комментарии в Ada "--", а формальные аннотации "--|") и вставляет определенные assert в нужных местах, то есть, насколько я понимаю таким образом они компилируют как бы debug версию, которая в run-time проверяет различные утверждения. Также формальные аннотации могут быть проверены формально, различными автоматическими верификаторами. Когда же нужно предоставить программу заказчику, то они компилируют release версию без дополнительных assert из ANNA. (Возможно, не совсем так, но я так понял).

Соответственно и для Oberon можно сделать формальные комментарии, которые относительно обычного компилятора будут просто комментариями, а специальный препроцессор (можно назвать его ANNO - ANNotated Oberon) сможет обрабатывать их и создавать специальную версию программы, которая будет работать и в то же время проверять саму себя.


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

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1447
Откуда: Киев
Вот в комментариях-то и дело. По опыту использования frama-c, в которой воплощена эта идея для C, могу сказать, что это плохо работает. Чтобы это не было мучением, язык должен воплощать возможность в себе.


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

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 987
Откуда: Казань
Тогда надо как в Eiffel, чтобы инварианты, предусловия и постусловия были в синтаксис языка встроены:
Код:
Loops

Loop ::=
      [Iteration]
      [Initialization]
      [Invariant]
      [Exit_condition]
      Loop_body
      [Variant]
      end

Iteration ::= across Expression as Identifier

Initialization ::= from Compound

Exit_condition ::= until Boolean_expression

Loop_body ::=
      loop Compound |
      all Boolean_expression |
      some Boolean_expression


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Виртуальный текст
СообщениеДобавлено: Среда, 26 Июль, 2017 23:13 
Аватара пользователя

Зарегистрирован: Суббота, 12 Июль, 2008 22:49
Сообщения: 575
Откуда: Россия, Санкт-Петербург
В язык JAVA встроена конструкция
Код:
assert <выражение>
, которая игнорируется компилятором при указании соответствующего ключа компилятора, однако все практические руководства советуют эту конструкцию не использовать.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Виртуальный текст
СообщениеДобавлено: Среда, 26 Июль, 2017 23:32 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1447
Откуда: Киев
По-видимому, они считают, что правильней кидать исключение.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Виртуальный текст
СообщениеДобавлено: Пятница, 28 Июль, 2017 00:30 
Аватара пользователя

Зарегистрирован: Суббота, 12 Июль, 2008 22:49
Сообщения: 575
Откуда: Россия, Санкт-Петербург
Так assert и кидает исключение.
Тут дело в том, что assert можно выключить как при компиляции, тогда его код даже не попадёт в финальный байткод, так и на JVM.
Получается что код вроде есть, но JVM его будет игнорировать.
Что бы не было неоднозначностей рекомендуют не пользоваться assert'ами, а использовать unit-test или явные проверки в коде


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Виртуальный текст
СообщениеДобавлено: Пятница, 28 Июль, 2017 11:56 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1447
Откуда: Киев
Madzi писал(а):
Так assert и кидает исключение
Тут дело в том, что assert можно выключить как при компиляции.

Кидает и может кидать - это не одно и то же.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Виртуальный текст
СообщениеДобавлено: Суббота, 29 Июль, 2017 01:05 
Аватара пользователя

Зарегистрирован: Суббота, 12 Июль, 2008 22:49
Сообщения: 575
Откуда: Россия, Санкт-Петербург
Ассерт если включен - всегда кидает при не выполнении логического выражения
Если выключен - какой с него спрос ?


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Виртуальный текст
СообщениеДобавлено: Понедельник, 31 Июль, 2017 13:45 
Аватара пользователя

Зарегистрирован: Воскресенье, 12 Апрель, 2015 18:12
Сообщения: 1134
Откуда: СССР v2.0 rc 1
Выключенные проверки -- плохие проверки.

Я вообще не понимаю смысла вводить систему исключений, если достаточно анализировать возвращаемое значение на подобный случай. В голанг ,имхо, сделан возврат несколько топорно, но это лучше чем фильтровать эксцепшены в питоне.

Что касается подхода ады/аннушки вс юнит-тесты, имхо, ты продумаешь 10 вариантов -- жизнь подкинет одиннадцатый. Тут я за методу Вальтера Николаевича -- локализовать ошибку как можно раньше, пока вся система не стартовала в космос. И положение №2: без греха программировал только Христос. Ах, пардон! Христос не программировал, значит безгрешных шкодеров не было, нет, и не будет.


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

Зарегистрирован: Вторник, 26 Январь, 2010 09:31
Сообщения: 717
Откуда: Барнаул
prospero78 писал(а):
локализовать ошибку как можно раньше, пока вся система не стартовала в космос.
Там-то нежданчик в виде сработавшего ASSERTа и нагрянет. И грохнется сей чудо-девайс прямо на башку прохожему.
А чтобы нежданчиков было как можно меньше и нужно юнит-тестирование, по завершении которого ASSERTы отключают.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Виртуальный текст
СообщениеДобавлено: Понедельник, 31 Июль, 2017 15:17 
Аватара пользователя

Зарегистрирован: Воскресенье, 12 Апрель, 2015 18:12
Сообщения: 1134
Откуда: СССР v2.0 rc 1
Kemet писал(а):
Там-то нежданчик в виде сработавшего ASSERTа и нагрянет. И грохнется сей чудо-девайс прямо на башку прохожему.
А чтобы нежданчиков было как можно меньше и нужно юнит-тестирование.

Ну не надо придумывать.
Для этого существует два этапа ввода в эксплуатацию. И, как показывает опыт "Протонов": вероятность того, что датчики направления прикручены кверху ногами будет раз в 10 выше, чем ошибка в работе вачдога, и ничего не слышно про косяки в софте на кросскомпиляторе ,-)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Виртуальный текст
СообщениеДобавлено: Понедельник, 31 Июль, 2017 17:42 

Зарегистрирован: Вторник, 26 Январь, 2010 09:31
Сообщения: 717
Откуда: Барнаул
Я тут глянул Report The Programming Language Oberon (Revision 1. 10. 90) и не нашел там ASSERT, только старый добрый HALT


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Виртуальный текст
СообщениеДобавлено: Понедельник, 31 Июль, 2017 22:24 
Аватара пользователя

Зарегистрирован: Воскресенье, 12 Апрель, 2015 18:12
Сообщения: 1134
Откуда: СССР v2.0 rc 1
Kemet писал(а):
Я тут глянул Report The Programming Language Oberon (Revision 1. 10. 90) и не нашел там ASSERT, только старый добрый HALT

Угу. Нету. Ассерт это процедура, которая пишется за одну секунду.
Проблема то в чём?
=Ссылочки давайте адекватные, плиз=
А вот тут есть. Страничка 3, будьте добры. В стандартных процедурах, как раз :lol:
Видимо, важный элемент языка для Николая Вальтеровича. И я почему-то с ним согласен))


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Виртуальный текст
СообщениеДобавлено: Вторник, 01 Август, 2017 06:34 

Зарегистрирован: Вторник, 26 Январь, 2010 09:31
Сообщения: 717
Откуда: Барнаул
prospero78 писал(а):
Kemet писал(а):
Я тут глянул Report The Programming Language Oberon (Revision 1. 10. 90) и не нашел там ASSERT, только старый добрый HALT

Угу. Нету. Ассерт это процедура, которая пишется за одну секунду.
Проблема то в чём?
=Ссылочки давайте адекватные, плиз=
А вот тут есть. Страничка 3, будьте добры. В стандартных процедурах, как раз :lol:
Видимо, важный элемент языка для Николая Вальтеровича. И я почему-то с ним согласен))
Ссылку я дал боле чем адекватную - Виртовский православный Оберон, в котором нет ASSERTа.
Получается ASSERT это не Вирт-Вэй, ога.
Это я к тому, что пихать ваши любимые ASSERTы куда ни попадя не стоит. Кстати, а кто считал, сколько ASSERTов поставил Вирт в новом проекте Оберон? Похоже, они там должны быть, как минимум, в каждой процедуре, раз это Вирт-Вэй!! А вот я счас проверю, хммм, что-то я их не вижу ((( Неужто Вирт нарушил свой же Вирт-Вэй???


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 23 ]  На страницу 1, 2  След.

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


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

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


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

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