DRAKON.SU https://forum.drakon.su/ |
|
Философия ДРАКОН-конструктора https://forum.drakon.su/viewtopic.php?f=164&t=4042 |
Страница 2 из 5 |
Автор: | Ильченко Эдуард [ Воскресенье, 05 Август, 2012 20:05 ] |
Заголовок сообщения: | Re: Философия ДРАКОН-конструктора |
Владимир Паронджанов писал(а): Эдуард, теорема у Вас перед глазами. Но, судя по всему, Вы ее просто не видите. Хотелось верить в чудо : ) Что доказательство этой теоремы ведёт и к доказательству (мною не улавливаемому) правильности алгоритма (хоть в какой-то части). Получается, что исчисление икон вещь сама в себе. Какую практическую ценность имеет строгое математическое доказательство правильности построения шампур-схемы-пустышки для доказательства алгоритма (который появится в будущем посредством заполнения икон)? Почему у меня появился этот вопрос? Вы сначала говорите о доказательстве правильности алгоритмов, а потом плавно переходите к утверждению об автоматическом доказательстве правильности шампур-схем (красным выделено мною). Владимир Паронджанов писал(а): Цитата: §10. ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ АЛГОРИТМОВ Роберт Андерсон подчеркивает: «целью многих исследований в области доказательства правильности программ является... механизация таких доказательств» [8]. Дэвид Грис указывает, что «доказательство должно опережать построение программы» [9]. … Дракон-конструктор осуществляет 100%-е автоматическое доказательство правильности шампур-схем, гарантируя принципиальную невозможность ошибок визуального синтаксиса. В результате у меня сложилось впечатление, что доказательство правильности шампур-схем каким-то образом способствует доказательству правильности алгоритма. Благодаря Вашему разъяснению, данному выше, я понял что это не так. |
Автор: | Ильченко Эдуард [ Воскресенье, 05 Август, 2012 22:53 ] |
Заголовок сообщения: | Re: Философия ДРАКОН-конструктора |
Владимир Паронджанов писал(а): Частичное доказательство правильности алгоритма с помощью дракон-конструктора осуществляется без какого-либо участия человека и достигается совершенно бесплатно... Ну, и ещё раз. Что именно, какая часть правильности алгоритма (НЕ СЛЕПЫША !) доказывается с помощью дракон-конструктора? Как пощупать руками эту часть? Хотелось бы пример. Вот цель. Вот исполнитель. Вот алгоритм его действий. Вот критерии оценки правильности алгоритма. Вот дракон-схема этого алгоритма. Вот в этой части дракон-схема доказывает (а не показывает!) правильность алгоритма. Я вижу, что дракон-схема показывает последовательность действий исполнителя. И совершенно не вижу как слепыш может хоть как-то гарантировать их правильность (за исключением разве что побочных входов в обычный цикл, да и то только если концептуально принять такое правило для алгоритмов (ведь и с побочными входами алгоритм может быть правильным)). |
Автор: | MaximGB [ Понедельник, 06 Август, 2012 02:49 ] |
Заголовок сообщения: | Re: Философия ДРАКОН-конструктора |
Насколько я понял из "Учитесь писать, читать и понимать алгоритмы" исчисление икон доказывает только что, при условии "сходимости" алгоритма, исполнитель точно доберётся из иконы "Начало" в икону "Конец". Под сходимостью я понимаю что иконы заполнены правильно на языке исполнителя и алгоритм выполнится за конечное количество шагов. Т.е. имея некую теорему зарисованную в исчислении икон как: Код: (Начало) | <условие>------------+ |да |нет ||Вставка 1|| ||Вставка 2|| | | +----------------+ | (Конец) Мы можем сделать вывод что она верна тогда и только тогда когда верны схемы соответствующие Вставке 1 и 2, и наоборот, если данная теорема верна, то Вставка 1 и Вставка 2 тоже должны быть верны Верны в смысле что есть маршрут из (Начало) в (Конец) |
Автор: | usr345 [ Понедельник, 06 Август, 2012 07:28 ] |
Заголовок сообщения: | Re: Философия ДРАКОН-конструктора |
Цитата: Я вижу, что дракон-схема показывает последовательность действий исполнителя. И совершенно не вижу как слепыш может хоть как-то гарантировать их правильность Дракон-схема лишь описывает алгоритм и не гарантирует, что в результате его выполнения мы получим нужный результат. Для доказательства корректности алгоритма нужно составить формальную спецификацию для результата алгоритма и формальную модель самого алгоритма. А потом доказать математическими методами, что алгоритм удовлетворяет требованиям формальной спецификации. Это довольно сложная процедура. http://en.wikipedia.org/wiki/Formal_verification |
Автор: | Alexey_Donskoy [ Понедельник, 06 Август, 2012 07:36 ] |
Заголовок сообщения: | Re: Философия ДРАКОН-конструктора |
Владислав Жаринов писал(а): Имеется в виду, нешампур-блок нельзя?.. ведь у шампур-блока по-любому вход и выход наружу торчат... Следует добавить "лишних связей" Формальное определение сами подберите. Что до "философии дракон-редактора", так надо изначально правильно ставить задачу. Ни в коем случае не "куда бы это можно приткнуть оторванный конец лианы?". Но обязательно: "Одним лёгким движением осуществлять допустимые топологические преобразования схемы". |
Автор: | Владислав Жаринов [ Вторник, 07 Август, 2012 08:32 ] |
Заголовок сообщения: | Re: Философия ДРАКОН-конструктора |
MaximGB писал(а): Насколько я понял из "Учитесь писать, читать и понимать алгоритмы" исчисление икон доказывает только что, при условии "сходимости" алгоритма, исполнитель точно доберётся из иконы "Начало" в икону "Конец". В общем да... Только "сходимость" - это завершаемость... для общего случая не имеющая алгоритма доказательства (см. проблему остановки алгоритма... хотя бы у Лаврова)...Под сходимостью я понимаю что иконы заполнены правильно на языке исполнителя и алгоритм выполнится за конечное количество шагов. ... Правильность заполнения икон - самостоятельное требование (доказываем что-либо для уже правильной на полном языке программы/спецификации)... впрочем, ставя "и" на естественном языке, Вы могли иметь в виду и это... |
Автор: | Владислав Жаринов [ Вторник, 07 Август, 2012 08:39 ] |
Заголовок сообщения: | Re: Философия ДРАКОН-конструктора |
Alexey_Donskoy писал(а): Владислав Жаринов писал(а): Имеется в виду, нешампур-блок нельзя?.. ведь у шампур-блока по-любому вход и выход наружу торчат... Следует добавить "лишних связей" Формальное определение сами подберите. ... Alexey_Donskoy писал(а): ... Согласен. Тогда при условии допущения операций с лианами у нас остаётся только путь, изложенный здесь: viewtopic.php?p=72238#p72238. Т.е. изначально сформулировать, "ЧТО есть правильная схема в любом возможном случае" - и заложить в редактор оперативный контроль условий правильности при неатомарных операциях - используя "буксируемые двойники" как динамическое отображение "лёгкого движения"... Что до "философии дракон-редактора", так надо изначально правильно ставить задачу. Ни в коем случае не "куда бы это можно приткнуть оторванный конец лианы?". Но обязательно: "Одним лёгким движением осуществлять допустимые топологические преобразования схемы". Если есть только вложение - то это не нужно. Ввод допвыходов типа исключения видимо, не считаем - это просто ещё контакты схемы с остальной моделью, как показано здесь... так?.. Над допвходами в стиле задачных входов, как они разобраны у Кауфмана: viewtopic.php?p=71991#p71991 надо, полагаю, ещё подумать... |
Автор: | Илья Ермаков [ Вторник, 07 Август, 2012 09:13 ] |
Заголовок сообщения: | Re: Философия ДРАКОН-конструктора |
Фактически, та правильность, о которой говорит В. Д. Паронджанов - это синтаксическая правильность, соответствие нарисованной схемы графовой грамматике. |
Автор: | Alexey_Donskoy [ Вторник, 07 Август, 2012 09:31 ] |
Заголовок сообщения: | Re: Философия ДРАКОН-конструктора |
Илья Ермаков писал(а): ...синтаксическая правильность, соответствие нарисованной схемы графовой грамматике. "Только программист может дать такой абсолютно точный и столь же бесполезный ответ". А то здесь никто не понимает про синтаксическую правильность, ага. Вопрос в том, что НАДО автоматически поддерживать эту правильность, и в том, как именно это обеспечить (в том числе в плане свободы пользовтаеля). И вопрос в том, что силуэт в принципе разрушает синтаксическую правильность, для поддержания которой в этом случае требуются нетривиальные и до сих пор чётко не определённые навороты. Топологическое преобразование графа из "примитива" в "силуэт" и обратно должно быть однозначным. А этого нет в нынешней форме языка. Поэтому он нарушает самим же собой продекларированные принципы. |
Автор: | Владислав Жаринов [ Вторник, 07 Август, 2012 09:38 ] |
Заголовок сообщения: | Эквиивалентность видов дракон-схем |
Alexey_Donskoy писал(а): ... Это да... а то описание вот в этом примере - не более, чем литературная зарисовка... дальнейший анализ выявил многообразие возможностей перехода... где-то писал об этом...
Топологическое преобразование графа из "примитива" в "силуэт" и обратно должно быть однозначным. А этого нет в нынешней форме языка. Поэтому он нарушает самим же собой продекларированные принципы. |
Автор: | Илья Ермаков [ Вторник, 07 Август, 2012 14:36 ] |
Заголовок сообщения: | Re: Философия ДРАКОН-конструктора |
Alexey_Donskoy писал(а): Топологическое преобразование графа из "примитива" в "силуэт" и обратно должно быть однозначным. А этого нет в нынешней форме языка. Поэтому он нарушает самим же собой продекларированные принципы. Ну а как Вы будете отображать автоматную логику без силуэта? Другой вопрос, что пропаганду использования межветочных циклов нужно бы признать неправильной. Т.е. если в программе есть явно выраженный традиционный цикл (а не случай переходов между состояниями), не должен он никогда быть раскиданным между ветками. Т.е. позволить веточный цикл только в рамках одной ветки (полезная вещь). |
Автор: | Владислав Жаринов [ Вторник, 07 Август, 2012 15:23 ] |
Заголовок сообщения: | Re: Философия ДРАКОН-конструктора |
Например, вот так... Кстати, в импер-части этого примера видно, что многоветочный цикл тоже м.б. (здесь - как "сверхцикл" по цепочке разных состояний)... но Вы имели в виду, полагаю, другое - не разрывать тело обычного цикла (в частности, представляющего одно состояние) на две и более веток. |
Автор: | Alexey_Donskoy [ Вторник, 07 Август, 2012 15:42 ] |
Заголовок сообщения: | Re: Философия ДРАКОН-конструктора |
Илья Ермаков писал(а): Другой вопрос, что пропаганду использования межветочных циклов нужно бы признать неправильной. Т.е. если в программе есть явно выраженный традиционный цикл (а не случай переходов между состояниями), не должен он никогда быть раскиданным между ветками. О том и речь.Уф-ф... Не прошло и пяти лет (или уже прошло? ). |
Автор: | Владислав Жаринов [ Вторник, 07 Август, 2012 15:48 ] |
Заголовок сообщения: | Re: Философия ДРАКОН-конструктора |
Чё-то упустил... И.Е. высказывался в пользу разрыва тел циклов между ветками силуэта?.. |
Автор: | Владимир Паронджанов [ Четверг, 09 Август, 2012 13:17 ] |
Заголовок сообщения: | Re: Философия ДРАКОН-конструктора |
Ильченко Эдуард в сообщении viewtopic.php?p=73759#p73759 писал(а): Хотелось верить в чудо. Что доказательство этой теоремы ведёт и к доказательству (мною не улавливаемому) правильности алгоритма (хоть в какой-то части). Да, ведет. Не полностью, а в некоторой части. В какой части? В части управляющих операторов. Ведь именно управляющие операторы преобразуются в шампур-схему. Ильченко Эдуард писал(а): Какую практическую ценность имеет строгое математическое доказательство правильности построения шампур-схемы-пустышки для доказательства алгоритма (который появится в будущем посредством заполнения икон)? Практическая ценность состоит в том, что шампур-схема (заменяющая управляющие операторы) оказывается безошибочной, гарантированно правильной.ПОЯСНЕНИЕ В самом деле, что происходит после заполнения икон? Шампур-схема превращается в алгоритм. Но! При заполнении икон управляющие операторы не записываются внутри икон. Они исчезают. Ведь их нигде нет. Они невидимы. Как это возможно? Это возможно потому, что управляющие операторы превратились в шампур-схему. Фокус в том, что управляющие операторы НЕ ИСЧЕЗЛИ, а ИЗМЕНИЛИ форму своего бытия. Они "ушли" из текстовой формы представления процедурных знаний. И "вошли" в графическую форму, то есть в форму шампур-схемы. Управляющие операторы полностью сохраняют свои фукции, будучи представленными в графической форме (в виде шампур-схемы). Можно сказать по-другому. Управляющие операторы инвариантны относительно преобразования "текстовая форма записи — графическая форма записи". ВЫВОД Цитата: Вопрос. Какую практическую ценность имеет строгое математическое доказательство правильности построения шампур-схемы-пустышки для доказательства алгоритма (который появится в будущем посредством заполнения икон)?
Ответ. Практическая ценность состоит в том, что управляющие операторы алгоритма, представленные в виде шампур-схемы оказываются безошибочными, гарантированно правильными. |
Автор: | Илья Ермаков [ Четверг, 09 Август, 2012 14:00 ] |
Заголовок сообщения: | Re: Философия ДРАКОН-конструктора |
Владимир Паронджанов писал(а): Практическая ценность состоит в том, что управляющие операторы алгоритма, представленные в виде шампур-схемы оказываются безошибочными, гарантированно правильными.[/b] [/quote]Владимир Даниелович, синтаксически безошибочными, но не семантически. Конструктор обеспечивает то же самое, что синтаксический анализатор обычных языков, но другим способом. А, например, методы Дейкстры или формальной верификации типа model-checking позволяют убедиться в том, что поведение программы соответствует спецификации требований. |
Автор: | Степан Митькин [ Четверг, 09 Август, 2012 15:18 ] |
Заголовок сообщения: | Re: Философия ДРАКОН-конструктора |
Илья Ермаков писал(а): Владимир Паронджанов писал(а): Конструктор обеспечивает то же самое, что синтаксический анализатор обычных языков, но другим способом. Разница между идеальным ДРАКОН-конструктором и компилятором обычного текстового языка вот в чём: - В случае с текстовой программой человек может написать всё, что угодно. А синтаксический анализатор потом проверит текст и укажет на ошибки. - В случае с конструктором человек не может нарисовать неправильную схему. Конструктор не даст. Поэтому и проверять потом ничего не надо. Если я правильно понял концепцию ДРАКОН-конструктора, она такова: 1) В каждый момент времени на листе находится правильная ДРАКОН схема. 2) Действия, разрешённые конструктором, приводят к изменённой, но тоже правильной ДРАКОН-схеме. То есть мы как бы едем по рельсам и можем переключать стрелки. Это даёт гарантию, что мы никогда не окажемся в чистом поле без дороги. Всегда будем на какой-нибудь станции. Это хорошая гарантия. Но у неё есть и минусы. Например: Пусть есть какая-то ДРАКОН-схема А. Я смотрю на неё, и она мне не нравится. Её нужно изменить так, чтобы получилась схема Б. Что делать? 1) В идеальном редакторе я должен придумать последовательность шагов, которые приведут схему из точки А в точку Б. Это тяжёлый умственный труд. 2) В графическом, свободном редакторе думать не надо. Можно просто передвинуть иконы туда, куда нужно. Мне не нравится идеальный конструктор, потому что я люблю рисовать. |
Автор: | Alexey_Donskoy [ Четверг, 09 Август, 2012 17:13 ] |
Заголовок сообщения: | Re: Философия ДРАКОН-конструктора |
Степан Митькин писал(а): Если я правильно понял концепцию ДРАКОН-конструктора, она такова: Это не концепция ДРАКОН-конструктора, а транзакция редактирования, до и после которой схема должна находиться в целостном (и правильном) состоянии.1) В каждый момент времени на листе находится правильная ДРАКОН схема. 2) Действия, разрешённые конструктором, приводят к изменённой, но тоже правильной ДРАКОН-схеме. Степан Митькин писал(а): 1) В идеальном редакторе я должен придумать последовательность шагов, которые приведут схему из точки А в точку Б. Это тяжёлый умственный труд. По моим оценкам, в среде Тышова до 70% ресурсов отнимает Степан Митькин писал(а): 2) В графическом, свободном редакторе думать не надо. Можно просто передвинуть иконы туда, куда нужно. Если при этом разрываются связи линий с блоками (как было в тех версиях, которые я смотрел), то это ХУЖЕ текстового редактора (не говоря уж о среде Тышова). В тексте хотя бы порядок сохраняется всегда, а тут периодически восстанавливать надо.Выводы: 1) если редактор не поддерживает транзакции редактирования, которые не могут быть завершены с нарушением синтаксиса - это плохой редактор; 2) если редактор поддерживает транзакции редактирования, которые обеспечивают прозрачное для пользователя сохранение (преобразование) семантики, это очень хороший редактор. Вашу среду пока можно дисквалифицировать по п.1 - нарушить синтаксис легко простым перетаскиванием элементов. Среда Тышова удовлетворяет п.1, но не п.2. Может показаться, что п.1 среда Тышова тоже не выполняет, поскольку часто бывают глюки при перетаскивании линий - сбоит автоматическая разводка, приходится исправлять вручную. Однако синтаксис при этих глюках не нарушается! П.2 частично выполняется средой Тышова. Например, рокировка в развилке удобно изменяет форму представления, сохраняя семантику. Но в чуть более сложных случаях, чем пара полностью вложенных развилок, подобное преобразование становится невозможным (или, по крайней мере, требующим пересечений). Вопрос, поднятый Эдуардом (о переносе петли цикла), вообще говоря, относится к п.2. Человек, желающий перенести петлю, может сделать это тремя путями: а) внести кусок кода в тело цикла (или вынести оттуда); б) переместить петлю; в) всё разобрать и собрать заново (как в Вашей среде со свободным рисованием) Очевидно, что вариант (в) рассматривать нет смысла, а варианты (а) и (б) топологически эквивалентны. Но тут я соглашусь с Паронджановым, что методически верно будет ставить задачу именно в формулировке (а) Соответственно, и редактор должен если не навязывать, то поощрять вариант (а)... |
Автор: | Владимир Паронджанов [ Четверг, 09 Август, 2012 18:04 ] |
Заголовок сообщения: | Re: Философия ДРАКОН-конструктора |
Илья Ермаков писал(а): Владимир Паронджанов писал(а): Практическая ценность состоит в том, что управляющие операторы алгоритма, представленные в виде шампур-схемы оказываются безошибочными, гарантированно правильными.[/b] Владимир Даниелович, синтаксически безошибочными, но не семантически. Уважаемый Илья Евгеньевич! Вы правы. И я с Вами согласен. Наши мысли во многом совпадают: Цитата: Дракон-конструктор осуществляет 100%-е автоматическое доказательство правильности шампур-схем, гарантируя принципиальную невозможность ошибок визуального синтаксиса. Вместе с тем возникает вопрос: Если ограничиться семантикой управляющих операторов, каким образом она (семантика) записывается в текстовой форме на ДРАКОНе? Ответ двоякий: 1. В виде надписей да и нет возле выходов иконы вопрос. Можно перепутать да и нет местами? Да, можно. Но вероятность этого невелика. 2. При записи условий внутри иконы вопрос. При записи условий тоже можно ошибиться. Но и здесь для защиты от ошибок есть специальные средства.
— Приведение дракон-схемы к каноническому виду. — Понятие "стандартная дракон-схема". — Понятие "нестандартная дракон-схема" и др. Перечисленные средства подробно описаны в книге "Учись..." в главе 11 Цитата: Глава 11. Логические формулы, используемые в алгоритмах ...153—183 ВЫВОДЫ 1. Для уменьшения вероятности ошибок в управляющих операторах в языке ДРАКОН используются синтаксические и семантические средства. 2. Синтаксические средства реализованы в дракон-конструкторе, который гарантирует невозможность ошибок визуального синтаксиса. 3. Семантические средства реализованы в виде дополнительных удобств для пользователя, которые хотя и не гарантируют безошибочность семантики управляющих операторов, но значительно снижают вероятность появления семантических ошибок в указанных операторах. 4. Таким образом, имеет место разумное сочетание метода доказательного программирования (исчисление икон) и специальных методов повышения надежности алгоритмов, реализованных в языке ДРАКОН. |
Автор: | Владислав Жаринов [ Пятница, 10 Август, 2012 08:04 ] |
Заголовок сообщения: | Re: Философия ДРАКОН-конструктора |
Владимир Даниелович, да ведь Илья Евгеньевич не об этом говорит. А о том, что программа д.б. корректна как целое - т.е. не только в импер-структурной части. Что с т.зр. получения требуемого от программы (а равно - информатизованной инструкции для "человека как машины") результата (допустимого соответствия множества вариантов использования на множестве вариаций исходных данных - притом коректно использующего ресурсы исполнителя) даёт соответствие "слепыша" правилам шампур-организации, если текст для заполнения "слепыша" (реально превращающий его в программу/инфор-инструкцию) сформулирован неверно?.. Например, какие-то выражения (т.е. импер-атрибутивная часть)... и/или атрибуция типов... я уже не говорю о типовой структуре, которую также на импер-"слепыше" не покажешь - тоже только текстом описывать, как Ярослав делает?.. Сама по себе - ничего не даёт. Только как часть целостного представления сочинителя о задаче в расчёте на принятого исполнителя (архитектуру машинной платформы, квалификацию человека). Теперь о синтаксической правильности для части целого (в данном случае - импер-структурной). Реализовали мы построение схем для этой части - и что? Алексей ведь правильно о тексте вспомнил - потому что так можно понять, что это даёт. А вот что - гарантию, что структура ключевых слов из той самой "тщательно обосновываемой коллекции" (напр. Дейкстрой для структурного программирования) будет всегда корректной по определению текстового инфор-языка, взятого для реализации. Скажем, какого-то ТЯП... или стандарта псевдокода. Т.е. в тексте, изоморфном схеме (а он д.б. всегда) эти слова будут образовывать корректные конструкции (проходимые для синтразбора). При этом остальное содержание целого (программы, инфор-инструкции) с т.зр. "слепышей" нужно считать ведь некими полями, параметризующими импер-структуру до целого. А вот чего там будет в этих полях - зависит уже от реализации других частей синтаксиса... И от того, что сформулирует сочинитель. А редактор, "заточенный" только на доказательность в импер-структурной части, эти остальные части никак не проверит... и корректность исполнения программы/инфор-инструкции как целого не установит... Притом заметим - синтаксис этих остальных частей м.б. ох каким разным... в своих РБНФ-определениях я ведь дал возможные варианты только примерно. Не говоря о том, что есть уровни семантики и способы их выражения (качественный - "родной", математический - напр., функциональный, информатический - высоко/низкоуровневый)... И им будут сотвествовать разные допустимые синтаксисы и в части импер-структур (скажем, на джамп-асме есть явные БП - а на ЯВУ м.б. и нет... зато ретурны м.б. - а выше в математической схеме порядок исполнения вообще иначе выражаться может)... Короче, для каждого конкретного языка правильность придётся уточнять. И будет у нас целое семейство стандартов на языки импер-"слепышей"... Т.е. мало сочинителю, чтобы редактор не дал ему нарисовать неправильную схему. Думать над семантикой целого и над её соответствием задаче всё равно надо... Замечу - и когда мы реализуем схемы для остальных частей целого (декларативной и активностной) - это останется в силе. В чём же плюс перехода от текста к графам для структурных частей? В том, о чём Вы не устаёте говорить - думать сочинителю часто оказывается легче... А формально доказывать правильность всё равно иначе надо - сочетанием тестирования и верификации... возможные методы И.Е. тже упомянул... |
Страница 2 из 5 | Часовой пояс: UTC + 3 часа |
Powered by phpBB® Forum Software © phpBB Group https://www.phpbb.com/ |