DRAKON.SU

Это, вообще говоря, хорошо. Разнообразие, конкуренция, научный поиск, не ограниченный "родительским авторитетом"...

И да, считаю, что давно назрела не просто реформа, а создание нового, исходя из обозначенных здесь требований и полученного опыта.

Слияние плеч http://drakon-editor.sourceforge.net/generation.html запрещать не обязательно, есть плюсы и минусы:
+ Слияние плеч явно не ухудшает структурируемость схемы, скорее улучшает.
- Слияние плеч требует излишнего кода в кодогенераторе. Например, Степан Митькин описал нормализацию, показанную на картинке.

Кстати, минус можно избежать, если генерить ассемблерный или машинный код прям из схемы.

Вот иллюстрация к моему примеру с алгоритмической ошибкой вида
0 GOTO 1
1 GOTO 0

Программа зацикливается.

К вопросу о веточном цикле:
Кто-то готов алгоритмически доказать, что веточный цикл не содержит таких цепочек?

Этой проблемы в ДРАКОНе не существует.
Вы вставляете иконы Вопрос, условные переходы, и почему-то считаете их безусловными переходами.

Подобная схема должна выглядеть так:

или даже так:

Но подобные конструкции отсутствуют в ДРАКОНе.

Минимальный код получается при использовании goto.

Я не считаю переходы безусловными. Я вижу условия, при которых схема зависает.

Именно! А далее приходим к тому, что необходимо запретить использовать язык Си ...

Теперь по вопросу Петра, веточному циклу и изображению конечного автомата.

Дракон должен управлять своим алгоритмом на основе событий. Есть икона таймера, которая может присоединяться слева. И тогда действие происходит по таймеру. Этого недостаточно!

Необходимо расширить смысл иконы: сделать ее Событие. Заметьте, что таймер слева лишь приостанавливает процесс, который потом возобновляется через интервал времени от 0 до Бесконечности.

Икона по событию может означать:
- событие от другого процесса/потока, как-то семафор, мьютекс
- действия оператора с оконной системой
- прерывание от системы В/В (пришли данные по сети)
- сигнал от ОС (SIGTERM)
- таймер как раньше

Я добавил сигналы об изменении 0, 1, 2: итогда та же схема становится правильной!

Из веточного цикла исключается обратная стрелка. Черных треугольников достаточно.

Веточный цикл может образовать бесконечную петлю прыжков назад. Если доказывается, что в петле, образуемой веточным циклом, не содержится зацикливающихся цепочек без икон Действие или Событие (слева), то веточный цикл использовать можно для данной схемы. А если есть такие цепочки, то нельзя.

Кстати, роль иконы Событие в С-примере играет ключевое слово volatile, которое нужно бы добавить

Спасибо. В будующем учту.

Дмитрий Викторович, я рад, что Вы ставите вопрос в острой форме и приветствую это. Потому что критика — воздух науки.

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

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

В разное время Вы, Дмитрий Викторович, разработали модели систем управления для тренажеров на основе языков стандарта МЭК 61131-3 (Functional Block Diagrams, Sequential Function Charts), экспертные системы обучения (симптомно-ориентированные инструкции) и диагностики (течи теплоносителя 1 контура), СКАДА-платформа СУОК и реализованные на ней общестанционные системы ИВС э/б 1 РоАЭС и 1 КлнАЭС.

Вместе с тем мне хотелось бы иметь опровергающий пример, подтверждающий преимущество традиционных принципов структурного программирования по сравнению с ДРАКОНом . Важность такого примера трудно переоценить.

Пока что такого опровергающего примера я не видел. В схемах Петра Приклонского я не заметил следов Вашего красного карандаша. Или, может быть, я что-то пропустил?

Вы имеете в виду, что если маршрут весь "пустой" и условия не содержат действий, то надо рассматривать переходы по ветвлениям как GOTO?..

P.S. Можно сказать, что здесь присутствуют ещё два БП - 1 GOTO 1 и 0 GOTO 0 - это которые с Адреса на однономерное Имя...

Уважаемый Владимир Даниелович!

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

Пока смогу сказать лишь то, что такая форма предполагает некоторые более развернутые последствия, надеюсь не такие революционные, как произошло с апрельскими тезисами.

Так это же и нужно доказывать на основе содержания икон... в части имён действий и величин... иначе как?..
Это можно пояснить на Вашем примере. Вводимое Событие (Сигнал) - это ведь и есть действие определённого типа, вводимое, чтобы сделать маршрут непустым... Но. Оно "расцикливает" (теоретически) лишь в том случае, если результаты события используются в охране хоть одной развилки на интересующем маршруте - раз и позволяют в случае изменения маршрута не "зациклиться" на другом маршруте - два. И выявляется это или доказательно, или проверкой моделей... или структурным анализом/синтезом, наверное... Но в любом случае мы привлекаем имена величин как минимум...
Тогда как проверить, нет ли пересечений в системе веточных циклов можно, ограничившись лишь их нумерацией вроде как (если предложенное здесь не содержит ошибок)...

Как я понял, ключевое слово volatile многим неизвестно.

Добавляю пару ссылок, разъясняющих проблему

http://www.pic24.ru/doku.php/osa/articl ... r_chainiks
http://chipenable.ru/index.php/programm ... atile.html

Исправленный ответ для Эдуарда Владимировича Ильченко

В сообщении viewtopic.php?p=80042#p80042 Эдуард Ильченко спросил:

В сообщении viewtopic.php?p=80052#p80052 Эдуард Ильченко повторил вопрос:


К сожалению, я не смог понять вопрос и ошибся, то есть ответил неправильно в сообщении viewtopic.php?p=80053#p80053
Вот мой НЕПРАВИЛЬНЫЙ ответ:


Эдуард Ильченко заметил мою ошибку и справедливо возмутился в сообщении viewtopic.php?p=80058#p80058


Признаю, что Эдуард Ильченко был прав, а я не прав.
Спешу исправить свою ошибку и предлагаю:
Правильный ответ. Адекватность обязательно должна рассматриваться.

Три шага проверки адекватности

Шаг 1. Исходный чертеж слепыша должен удовлетворять правилам графического синтаксиса языка ДРАКОН. Это значит, для проверки адекватности необходимо убедиться, что слепыш строго соответствует правилам графического синтаксиса. Если соответствия нет, то говорить об адекватности нельзя.

Шаг 2. Транслятор должен реализовывать правила графического синтаксиса, формализованные в логическом исчислении икон. Если транслятор не удовлетворяет указанным правилам, то говорить об адекватности нельзя.

Шаг 3. Практическая проверка адекватности работы правильно спроектированного транслятора осуществляется тестированием с помощью набора тестов и проверенного оригинала (слепыша).

Поддержу Дмитрия Дагаева, так же и Алексея Донского. И если уж говорить о строгом математическом формализме, то их правоту подтверждают теоремы Гёделя о неполноте.

Вряд ли здесь можно говорить о каком-то уровне семантической корректности программы выше, чем просто отсутствие синтаксических противоречий (хотя это тоже часть доказательства верной семантики, но только малая часть). И одного эргономичного визуального восприятия явно недостаточно, чтобы быть уверенным в корректности. Система исчисления икон далека до уровня, к примеру, темпоральной логики. Мне недавно на глаза попался документик: Analyzing Singularity Channel Contracts. В нём небольшое описание исследования контрактов каналов для взаимодействия процессов в Singularity - экспериментальной ОС от Майкрософт. В этой операционке изолированные процессы взаимодействуют через обмен сообщениями с помощью каналов для их передачи. Каналы имеют контракты - интерфейсы, определяющие список событий, состояний, порядок отправки/приёмки сигналов и пр., которых должны строго придерживаться ничего не знающие о друг друге процессы-серверы и процессы-клиенты. У меня огромные сомнения в том, что если бы проектирование этих интерфейсов осуществлялось с помощью ДРАКОНа, то он бы наглядно показал (а в идеале - автоматически выявил бы) те косяки разработчиков (насчёт взаимоблокировок), которые определили исследователи через формальную верификацию.

Кстати, здесь задача насчёт корректности - полный ахтунг. В качестве примера (кроме тотального тестирования) - CompCert - верифицирующий С-компилятор (с ограничениями), который занимается формальным доказательством соответствия генерируемого бинарного кода семантике исходного текста. Думаю, что на базе этого проекта (и Coq, известного доказателя теорем, которого используют для верификации) выдали не одну диссертацию, особенно учитывая истоки разработчиков этих проектов.

Исправленный ответ для Геннадия Николаевича Тышова.


К сожалению, я погорячился и ошибся, то есть ответил Геннадию Тышову неправильно в сообщении viewtopic.php?p=80039#p80039

Вот мой НЕПРАВИЛЬНЫЙ ответ:


Моя ошибка состоит в том, что я на себя наговорил.
Суть в том, что некорректности НЕТ. Все абсолютно корректно и математически строго.

Спешу исправить свою ошибку и предлагаю:
Правильный ответ.

Я придаю большое значение этой теме.

ЧТО ТАКОЕ ШАМПУР-СХЕМА? Это дракон-схема, из которой удален текст.

Шампур-схема — это абстракция, высокий уровень абстракции.

В чем смысл этой абстракции? Шампур-схема — это не одна программа, а класс программ.

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

Шампур-схема — это строго доказанная теорема. Следовательно, все программы, входящие в данный класс программ, имеют общее свойство — они имеют безошибочную графику.

Некоторым аналогом понятия "шампур-схема" является понятие "крупноблочная схема", введенное Виктором Николаевичем Касьяновым.

В 100500-й раз повторяю: Вы совершенно неуместно, с явным полемическим подтекстом, используете термин "безошибочность".
Речь здесь идёт о соответствии некоей конструкции формальному синтаксису некоего языка. Всё! Не более того.

Какой смысл об этом рассуждать вообще?
Тем более, какой смысл добавлять, что это соответствие, раз уж оно есть, - "безошибочно"?

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