DRAKON.SU

Какие существуют методы верификации программ (алгоритмов) записанных на ДРАКОНЕ?

Тестирование с помощью распечатки и карандаша : )

Отвечать надо подробно. Эдуард Ильченко дал правильный, но не полный ответ.

В чем неполнота?

В том, что ДРАКОН (за исключением некоторых случаев) дает гарантию отсутствия ошибок. Какую гарантию? Математическую.

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

Сегодня редактор Геннадия Тышова реализует указанное исчисление. А редактор Степана Митькина не реализует.

Безошибочность является принципиальным отличием языка ДРАКОН. Достигается эта безошибочность большим трудом, который должны затратить разработчики дракон-редактора.

Подробнее см.
viewtopic.php?t=4350
https://forum.oberoncore.ru/viewtopic.php?f=62&t=4350

=======================

Исправленный ответ для Эдуарда Ильченко дан здесь:
http://forum.oberoncore.ru/viewtopic.php?p=82806#p82806

Хорошо, есть математически точное доказательство основанное на "исчислении икон". Приведите, пожалуйста, какой-нибудь небольшой пример, где математически строго доказывается корректность алгоритма, основанного на данном методе.

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

2. Речь идет о визуальном логическом исчислении.

3. Математическое доказательство приведено здесь (см. стр. 427 — 433).
http://drakon.su/_media/biblioteka/chas ... drakon.pdf

4. Примеры показаны здесь (см. стр. 396 — 408):
http://drakon.su/_media/biblioteka/chas ... isanie.pdf

5. Преобразуя аксиомы (заготовки) на рис. 232 по формальным правилам получаем доказанные теоремы (пустые дракон-схемы) которые являются корректными (безошибочными).

6. Простые примеры показаны на рис. 233 — 238.
Более сложный пример показан на рис. 239 — 241.

http://rudocs.exdat.com/docs/index-571996.html?page=5


ИС Дракон позволит спроектировать графический алгоритм соответствующий спецификации, привлечь для этого прикладных специалистов.

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

При этом мы имеем разделение труда во времени и исполнителям, за полноту и логику алгоритма ответственен прикладной специалист, за внутреннее представление ответственен программист.

Допустим есть алгоритм нахождения частного и остатка от деления двух положительных чисел.
Взял блок-схему из книги Вирта "Систематическое программирование" (рисунок во вложении). Данная схема снабжена комментариями, в виде утверждений, которые выполняются в каждой точке алгоритма.
Какие своства данного алгоритма можно было бы доказать с помощью исчисления икон, если бы данный алгоритм был записан на ДРАКОНЕ?

Только последовательность выполнения операторов (икон). При этом совершенно неважно, что записано в иконах. Эта последовательность икон может вообще не иметь отношения к данному алгоритму. В отрыве от текстового наполнения икон и замысла программиста, доказанная правильность выполнения последовательности икон не имеет практического значения. Все ошибки будут скрываться в тексте и связях между иконами, которые устанавливает программист. ДРАКОНу всё равно, куда указывает связь (с учётом правил). Т.е. ДРАКОН-схема будет 28 раз правильной, а алгоритм ни разу не правильный (с учётом заданной цели алгоритма).

Поэтому, бумага и карандаш (или их электронные аналоги : )

Согласен.
При этом следует обязательно добавить, что речь идет не только о линейной последовательности, но и о ЛЮБОЙ последовательности, включая разветвления и циклы.

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

Не согласен. Доказанная правильность выполнения последовательности икон ИМЕЕТ практическое значение, причем очень большое.

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

Согласен.

Согласен. Теоретически такое действительно возможно, но на практике вероятность данного события ничтожна; поэтому ей можно пренебречь.

==========================

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

Я утверждаю, что ДРАКОН является БЕЗОШИБОЧНЫМ (в том смысле, что вероятность появления ошибок существенно уменьшается при условии, что дракон-редактор спроектирован правильно и полностью реализует логическое исчисление икон). БЕЗОШИБОЧНОСТЬ — главное достоинство языка ДРАКОН.

Эдуард Ильченко утверждает, что использование ДРАКОНа не приводит к уменьшению числа ошибок.

=======================

Примечание

Шампур-схема аналогична классу "крупноблочных схем", если использовать терминологию Виктора Николаевича Касьянова.
Приведу цитату из его книги "Оптимизирующие преобразования программ" М.: Наука, 1988. — 336с. — С. 35. — ISBN 5-02-013778-2


Цитата:
2. Класс крупноблочных схем

Крупноблочная схема программы может быть представлена в виде текста на некотором языке «полипрограммирования», который в отличие от обычного языка программирования допускает семантическую неоднозначность данных и операций. Фиксация одной из возможных интерпретаций превращает крупноблочную схему, которая до этого времени является «полипрограммой» (описанием целого множества крупноблочных программ, имеющих одну и ту же структуру), в конкретную программу для некоторой гипотетической вычислительной машины, например, РАМ.


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

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

Так наверное предикаты тоже можно вставлять в виде развилки? Или это не то?

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

Я этого не утверждал.
Я утверждаю, что ДРАКОН ПРИВОДИТ к уменьшению числа ошибок.
Но это происходит не в области "правильных редакторов", а в области психологии (восприятия) человеком ДРАКОН-схем. Особенно помогает самостоятельное конструирование схем : )

Да, конечно.
Но алгоритм развёрнутый во времени - линейная последовательность.

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

На практике ситуация такая: я разрабатываю алгоритм, в ходе разработки получаю некоторое количество правильных ДРАКОН-схем, которые кажутся сначала правильной схемой алгоритма, а чуть попозже неправильной : ) И только я (субъективно) решаю, что схема алгоритма стала адекватной поставленной цели.

Можно сказать и так: любая ДРАКОН-схема представляет правильный алгоритм, но при этом он может не соответствовать поставленной цели. Соответственно, ДРАКОН-схема не доказывает правильность алгоритма заявленной цели.

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

Согласен.

Частично согласен, частично нет.
Согласен с тем, что «это происходит … в области психологии (восприятия) человеком ДРАКОН-схем».
Не согласен с утверждением, что «это происходит не в области "правильных редакторов"».

РАЗБОР ПОЛЕТОВ
(подробная аргументация)

Я согласен с Эдуардом Ильченко, что ДРАКОН приводит к уменьшению числа ошибок.

Возникает вопрос: в чем причина этого? Почему ДРАКОН приводит к уменьшению числа ошибок?

Первая причина психологическая. Дело в том, что ДРАКОН улучшает восприятие алгоритма, ошибки становятся более заметными; с помощью дракон-схем их легче обнаружить и исправить. Мы оба (Эдуард Ильченко и я) с этим согласны.

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

Если дракон-редактор реализует исчисление икон, ошибок в графике не будет. Если же это требование не выполняется, то математическая гарантия исчезает.
И что дальше?

Последствия неблагоприятны — дракон-редактор перестает следить за соблюдением правил. В результате происходит катастрофа — неопытный пользователь может наломать дров и наделать множество ошибок (которые «умный» дракон-редактор НИКОГДА В ЖИЗНИ не позволит ему натворить).

ВОЗНИКАЕТ ВОПРОС:
КТО БУДЕТ СЛЕДИТЬ ЗА СОБЛЮДЕНИЕМ ПРАВИЛ,
ЕСЛИ ДРАКОН-РЕДАКТОР "ЗАБАСТУЕТ"
И ОТКАЖЕТСЯ ВЫПОЛНЯТЬ ИСЧИСЛЕНИЕ ИКОН?

В этом случае все обязанности по контролю за соблюдением правил возлагаются на бедного пользователя.
При этом возникает серьезная проблема.

Дело в том, что у ДРАКОНа великое множество правил. Выучить эту бездну правил очень трудно. Это высокий порог, одолеть который сможет далеко не каждый. Заблудившись в лабиринте правил, многие люди придут к (ошибочному) выводу, что ДРАКОН слишком сложен и годится только для яйцеголовых, а простым смертным он не по плечу.

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

Конечно, надо поступить по-другому. Груз надо снять с человека и перекинуть на программу "дракон-редактор".
Последний будет следить за соблюдением правил автоматически, аккуратно и методично выполняя правила, предписанные логическим исчислением икон.

Множество правил ДРАКОНа должен запоминать не человек, а его верный раб — автоматический дракон-редактор. Проще говоря, человек вовсе не обязан зубрить все правила и затем мучительно соображать, куда можно, у куда нельзя вести линию на дракон-схеме. Ничего этого не нужно. Потому что умный редактор не даст глупому пользователю сойти с рельсов и сбиться с пути.

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

В самом деле, уважаемый Геннадий Николаевич Тышов занимается этим свыше пяти лет, и работа в полной мере еще не завершена. Потому что это очень трудная работа. Такую работу раньше никто не делал.

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

Дракон позволяет получить ясный и логически правильный алгоритм, но это еще не означает, что полученная программа будет надежно работать.
Снижается лишь вероятность логических ошибок, но вероятность синтаксических (ошибки в операторах и присвоениях) и семантических ошибок (недопустимые значения величин) такая же как и в обычных языках.

Для примера недавно писал программу УЗИ датчика на Си с использованием предварительного построения алгоритма в Drakon Editor. Алгоритм получился хороший, после отладки все заработало безупречно.
Но отлаживать программу пришлось как обычно, т.е. довольно долго. Я одновременно допустил одну синтаксическую ошибку (забыл операнд в сумме) и две семантические (переменную для суммы взял типа double а не int) и в функции itoa было задано слишком мало элементов для символьного массива. В результате происходило переполнение и срыв стека при больших значениях параметров.