DRAKON.SU

Текущее время: Воскресенье, 26 Июнь, 2022 20:43

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




Начать новую тему Ответить на тему  [ Сообщений: 16 ] 
Автор Сообщение
СообщениеДобавлено: Среда, 09 Октябрь, 2013 15:33 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 219
Откуда: Казань
Какие существуют методы верификации программ (алгоритмов) записанных на ДРАКОНЕ?


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 09 Октябрь, 2013 15:57 

Зарегистрирован: Понедельник, 09 Ноябрь, 2009 17:29
Сообщения: 904
Откуда: Россия, Питер
Rifat писал(а):
Какие существуют методы верификации программ (алгоритмов) записанных на ДРАКОНЕ?

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 09 Октябрь, 2013 18:06 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 5434
Откуда: Москва
Rifat писал(а):
Какие существуют методы верификации программ (алгоритмов) записанных на ДРАКОНЕ?


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

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

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

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

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

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

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

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

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 09 Октябрь, 2013 18:48 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 219
Откуда: Казань
Хорошо, есть математически точное доказательство основанное на "исчислении икон". Приведите, пожалуйста, какой-нибудь небольшой пример, где математически строго доказывается корректность алгоритма, основанного на данном методе.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 09 Октябрь, 2013 19:13 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 5434
Откуда: Москва
Rifat писал(а):
Приведите, пожалуйста, какой-нибудь небольшой пример, где математически строго доказывается корректность алгоритма, основанного на данном методе.


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.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 09 Октябрь, 2013 20:50 

Зарегистрирован: Воскресенье, 06 Апрель, 2008 14:43
Сообщения: 1657
http://rudocs.exdat.com/docs/index-571996.html?page=5
Цитата:
Отказ ПО обусловлен несоответствием ПО поставленным задачам.

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

^ Корректность программы – ее соответствие спецификации.


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

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

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 10 Октябрь, 2013 08:25 

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


Вложения:
alg.png
alg.png [ 54.31 КБ | Просмотров: 13149 ]
Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 10 Октябрь, 2013 11:50 

Зарегистрирован: Понедельник, 09 Ноябрь, 2009 17:29
Сообщения: 904
Откуда: Россия, Питер
Ильченко Эдуард писал(а):
Rifat писал(а):
Какие существуют методы верификации программ (алгоритмов) записанных на ДРАКОНЕ?

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


Владимир Паронджанов писал(а):
Отвечать надо подробно. Эдуард Ильченко дал правильный, но не полный ответ.


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

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 10 Октябрь, 2013 16:18 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 5434
Откуда: Москва
Ильченко Эдуард писал(а):
Только последовательность выполнения операторов (икон). При этом совершенно неважно, что записано в иконах.
Согласен.
При этом следует обязательно добавить, что речь идет не только о линейной последовательности, но и о ЛЮБОЙ последовательности, включая разветвления и циклы.

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

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

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

Ильченко Эдуард писал(а):
ДРАКОНу всё равно, куда указывает связь (с учётом правил).
Согласен.

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

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

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

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

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


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

                Примечание

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

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

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


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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 10 Октябрь, 2013 21:33 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 219
Откуда: Казань
Как я понял, правы и Ильченко Эдуард и Владимир Паронджанов, каждый по-своему. Если блоки сильно зависимы друг от друга по данным, как в моем примере с вычислением частного, то доказательство порядка выполнения действий мало что дает, здесь лучше применить исчисление предикатов. Если же блоки не сильно связаны друг с другом по данным, например, в случае с самолетом: одно действие - открыть люк шасси, а второе действие - выпуск шасси, то доказательство последовательности действий имеет практический смысл. Если, допустим, докажем, что ни при каких обстоятельствах шасси не будет выпущено раньше, чем откроется люк для шасси, здесь прав Владимир Паронджанов.
Лично мне чаще приходится иметь дело с первым случаем, когда действия сильно связаны друг с другом по данным.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 11 Октябрь, 2013 06:35 

Зарегистрирован: Суббота, 16 Февраль, 2008 07:58
Сообщения: 239
Откуда: Россия, Стерлитамак
Так наверное предикаты тоже можно вставлять в виде развилки? Или это не то?


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 11 Октябрь, 2013 07:37 

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 11 Октябрь, 2013 07:44 

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 11 Октябрь, 2013 08:36 

Зарегистрирован: Понедельник, 09 Ноябрь, 2009 17:29
Сообщения: 904
Откуда: Россия, Питер
Владимир Паронджанов писал(а):
Ильченко Эдуард писал(а):
Только последовательность выполнения операторов (икон). При этом совершенно неважно, что записано в иконах.
Согласен.
При этом следует обязательно добавить, что речь идет не только о линейной последовательности, но и о ЛЮБОЙ последовательности, включая разветвления и циклы.
Да, конечно.
Но алгоритм развёрнутый во времени - линейная последовательность.

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

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

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

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 11 Октябрь, 2013 16:31 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 5434
Откуда: Москва
В сообщении viewtopic.php?p=82898#p82898 Ильченко Эдуард в последнем абзаце писал(а):
Я утверждаю, что ДРАКОН ПРИВОДИТ к уменьшению числа ошибок.
Согласен.

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

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


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

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

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

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

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

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

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


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

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

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

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

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

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

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

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Суббота, 12 Октябрь, 2013 19:43 

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

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


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

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


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

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


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

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