OberonCore
https://forum.oberoncore.ru/

Виртуальный текст
https://forum.oberoncore.ru/viewtopic.php?f=82&t=6088
Страница 1 из 2

Автор:  Rifat [ Вторник, 25 Июль, 2017 16:54 ]
Заголовок сообщения:  Виртуальный текст

Несколько лет назад было обсуждение:
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.
Как думаете, будет ли полезен подобный механизм виртуального текста для языка Оберон?

Автор:  Comdiv [ Вторник, 25 Июль, 2017 18:12 ]
Заголовок сообщения:  Re: Виртуальный текст

Дадите пример?

Автор:  Илья Ермаков [ Среда, 26 Июль, 2017 10:29 ]
Заголовок сообщения:  Re: Виртуальный текст

Мы у себя в АСУТП что-то типа простого Self-Checking-а тоже применяем.
Каждый Оберон-мессидж имеет процедуру Check, состояние любого объекта тоже имеет процедуру валидации - и эти валидации выполняются как при прохождении мессиджей, так и при установке нового состояния объекта после такта работы логики.

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

Примеры кода на ANNA (ANNotations for Ada):
Вложение:
anna1.png
anna1.png [ 46.16 КБ | Просмотров: 6099 ]

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

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

Теперь ясно. Да, нужно, но не для Oberon, потому что, по-хорошему, такие вещи должны быть учтены в языке сразу, а это уже не Oberon.

Автор:  prospero78 [ Среда, 26 Июль, 2017 12:14 ]
Заголовок сообщения:  Re: Виртуальный текст

Рифат ,мы всё ещё возвращаемся к проблеме "верификация верификатора". В Обероне есть пред- и пост- условия + строгая типизация + проверка границ структур данных этапа исполнения + сборщик мусора.
По сути, 90% всех ошибок -- это последние две килл-фичи Оберона.

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

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

В книге "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) сможет обрабатывать их и создавать специальную версию программы, которая будет работать и в то же время проверять саму себя.

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

Вот в комментариях-то и дело. По опыту использования frama-c, в которой воплощена эта идея для C, могу сказать, что это плохо работает. Чтобы это не было мучением, язык должен воплощать возможность в себе.

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

Тогда надо как в 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

Автор:  Madzi [ Среда, 26 Июль, 2017 23:13 ]
Заголовок сообщения:  Re: Виртуальный текст

В язык JAVA встроена конструкция
Код:
assert <выражение>
, которая игнорируется компилятором при указании соответствующего ключа компилятора, однако все практические руководства советуют эту конструкцию не использовать.

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

По-видимому, они считают, что правильней кидать исключение.

Автор:  Madzi [ Пятница, 28 Июль, 2017 00:30 ]
Заголовок сообщения:  Re: Виртуальный текст

Так assert и кидает исключение.
Тут дело в том, что assert можно выключить как при компиляции, тогда его код даже не попадёт в финальный байткод, так и на JVM.
Получается что код вроде есть, но JVM его будет игнорировать.
Что бы не было неоднозначностей рекомендуют не пользоваться assert'ами, а использовать unit-test или явные проверки в коде

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

Madzi писал(а):
Так assert и кидает исключение
Тут дело в том, что assert можно выключить как при компиляции.

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

Автор:  Madzi [ Суббота, 29 Июль, 2017 01:05 ]
Заголовок сообщения:  Re: Виртуальный текст

Ассерт если включен - всегда кидает при не выполнении логического выражения
Если выключен - какой с него спрос ?

Автор:  prospero78 [ Понедельник, 31 Июль, 2017 13:45 ]
Заголовок сообщения:  Re: Виртуальный текст

Выключенные проверки -- плохие проверки.

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

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

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

prospero78 писал(а):
локализовать ошибку как можно раньше, пока вся система не стартовала в космос.
Там-то нежданчик в виде сработавшего ASSERTа и нагрянет. И грохнется сей чудо-девайс прямо на башку прохожему.
А чтобы нежданчиков было как можно меньше и нужно юнит-тестирование, по завершении которого ASSERTы отключают.

Автор:  prospero78 [ Понедельник, 31 Июль, 2017 15:17 ]
Заголовок сообщения:  Re: Виртуальный текст

Kemet писал(а):
Там-то нежданчик в виде сработавшего ASSERTа и нагрянет. И грохнется сей чудо-девайс прямо на башку прохожему.
А чтобы нежданчиков было как можно меньше и нужно юнит-тестирование.

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

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

Я тут глянул Report The Programming Language Oberon (Revision 1. 10. 90) и не нашел там ASSERT, только старый добрый HALT

Автор:  prospero78 [ Понедельник, 31 Июль, 2017 22:24 ]
Заголовок сообщения:  Re: Виртуальный текст

Kemet писал(а):
Я тут глянул Report The Programming Language Oberon (Revision 1. 10. 90) и не нашел там ASSERT, только старый добрый HALT

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

Автор:  Kemet [ Вторник, 01 Август, 2017 06:34 ]
Заголовок сообщения:  Re: Виртуальный текст

prospero78 писал(а):
Kemet писал(а):
Я тут глянул Report The Programming Language Oberon (Revision 1. 10. 90) и не нашел там ASSERT, только старый добрый HALT

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

Страница 1 из 2 Часовой пояс: UTC + 3 часа
Powered by phpBB® Forum Software © phpBB Group
https://www.phpbb.com/