DRAKON.SU

Текущее время: Вторник, 19 Март, 2024 11:12

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




Начать новую тему Ответить на тему  [ Сообщений: 81 ]  На страницу Пред.  1, 2, 3, 4, 5  След.
Автор Сообщение
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Воскресенье, 05 Август, 2012 20:05 

Зарегистрирован: Понедельник, 09 Ноябрь, 2009 17:29
Сообщения: 904
Откуда: Россия, Питер
Владимир Паронджанов писал(а):
Эдуард, теорема у Вас перед глазами. Но, судя по всему, Вы ее просто не видите.

Хотелось верить в чудо : ) Что доказательство этой теоремы ведёт и к доказательству (мною не улавливаемому) правильности алгоритма (хоть в какой-то части).

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

Почему у меня появился этот вопрос?

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

Владимир Паронджанов писал(а):
Цитата:
§10. ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ АЛГОРИТМОВ

Роберт Андерсон подчеркивает: «целью многих исследований в области доказательства правильности программ является... механизация таких доказательств» [8]. Дэвид Грис указывает, что «доказательство должно опережать построение программы» [9].

Дракон-конструктор осуществляет 100%-е автоматическое доказательство правильности шампур-схем, гарантируя принципиальную невозможность ошибок визуального синтаксиса.


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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Воскресенье, 05 Август, 2012 22:53 

Зарегистрирован: Понедельник, 09 Ноябрь, 2009 17:29
Сообщения: 904
Откуда: Россия, Питер
Владимир Паронджанов писал(а):
Частичное доказательство правильности алгоритма с помощью дракон-конструктора осуществляется без какого-либо участия человека и достигается совершенно бесплатно...

Ну, и ещё раз.
Что именно, какая часть правильности алгоритма (НЕ СЛЕПЫША !) доказывается с помощью дракон-конструктора? Как пощупать руками эту часть?

Хотелось бы пример.

Вот цель.
Вот исполнитель.
Вот алгоритм его действий.
Вот критерии оценки правильности алгоритма.
Вот дракон-схема этого алгоритма.
Вот в этой части дракон-схема доказывает (а не показывает!) правильность алгоритма.

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Понедельник, 06 Август, 2012 02:49 

Зарегистрирован: Вторник, 20 Ноябрь, 2007 10:45
Сообщения: 31
Насколько я понял из "Учитесь писать, читать и понимать алгоритмы" исчисление икон доказывает только что, при условии "сходимости" алгоритма, исполнитель точно доберётся из иконы "Начало" в икону "Конец".
Под сходимостью я понимаю что иконы заполнены правильно на языке исполнителя и алгоритм выполнится за конечное количество шагов.
Т.е. имея некую теорему зарисованную в исчислении икон как:
Код:
     (Начало)
         |
     <условие>------------+
         |да              |нет
   ||Вставка 1||    ||Вставка 2||
         |                |
         +----------------+
         |
      (Конец)

Мы можем сделать вывод что она верна тогда и только тогда когда верны схемы соответствующие Вставке 1 и 2, и наоборот, если данная теорема верна, то Вставка 1 и Вставка 2 тоже должны быть верны ;) Верны в смысле что есть маршрут из (Начало) в (Конец)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Понедельник, 06 Август, 2012 07:28 

Зарегистрирован: Понедельник, 09 Август, 2010 22:28
Сообщения: 128
Цитата:
Я вижу, что дракон-схема показывает последовательность действий исполнителя.
И совершенно не вижу как слепыш может хоть как-то гарантировать их правильность


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

Это довольно сложная процедура.

http://en.wikipedia.org/wiki/Formal_verification


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Понедельник, 06 Август, 2012 07:36 
Аватара пользователя

Зарегистрирован: Суббота, 29 Март, 2008 19:27
Сообщения: 1098
Откуда: Россия, Чебоксары
Владислав Жаринов писал(а):
Имеется в виду, нешампур-блок нельзя?.. ведь у шампур-блока по-любому вход и выход наружу торчат... :)
Следует добавить "лишних связей" :D
Формальное определение сами подберите. :wink:

Что до "философии дракон-редактора", так надо изначально правильно ставить задачу.
Ни в коем случае не "куда бы это можно приткнуть оторванный конец лианы?".
Но обязательно: "Одним лёгким движением осуществлять допустимые топологические преобразования схемы".


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Вторник, 07 Август, 2012 08:32 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 1443
MaximGB писал(а):
Насколько я понял из "Учитесь писать, читать и понимать алгоритмы" исчисление икон доказывает только что, при условии "сходимости" алгоритма, исполнитель точно доберётся из иконы "Начало" в икону "Конец".
Под сходимостью я понимаю что иконы заполнены правильно на языке исполнителя и алгоритм выполнится за конечное количество шагов.
...
В общем да... Только "сходимость" - это завершаемость... для общего случая не имеющая алгоритма доказательства (см. проблему остановки алгоритма... хотя бы у Лаврова)...
Правильность заполнения икон - самостоятельное требование (доказываем что-либо для уже правильной на полном языке программы/спецификации)... впрочем, ставя "и" на естественном языке, Вы могли иметь в виду и это...


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Вторник, 07 Август, 2012 08:39 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 1443
Alexey_Donskoy писал(а):
Владислав Жаринов писал(а):
Имеется в виду, нешампур-блок нельзя?.. ведь у шампур-блока по-любому вход и выход наружу торчат... :)
Следует добавить "лишних связей" :D
Формальное определение сами подберите. :wink:
...
Я говорю о "нелинейных" связях в этом случае... :)
Alexey_Donskoy писал(а):
...
Что до "философии дракон-редактора", так надо изначально правильно ставить задачу.
Ни в коем случае не "куда бы это можно приткнуть оторванный конец лианы?".
Но обязательно: "Одним лёгким движением осуществлять допустимые топологические преобразования схемы".
Согласен. Тогда при условии допущения операций с лианами у нас остаётся только путь, изложенный здесь: viewtopic.php?p=72238#p72238. Т.е. изначально сформулировать, "ЧТО есть правильная схема в любом возможном случае" - и заложить в редактор оперативный контроль условий правильности при неатомарных операциях - используя "буксируемые двойники" как динамическое отображение "лёгкого движения"... :)

Если есть только вложение - то это не нужно. Ввод допвыходов типа исключения видимо, не считаем - это просто ещё контакты схемы с остальной моделью, как показано здесь... так?..
Над допвходами в стиле задачных входов, как они разобраны у Кауфмана: viewtopic.php?p=71991#p71991 надо, полагаю, ещё подумать...


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Вторник, 07 Август, 2012 09:13 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 631
Откуда: Россия, Орёл
Фактически, та правильность, о которой говорит В. Д. Паронджанов - это синтаксическая правильность, соответствие нарисованной схемы графовой грамматике.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Вторник, 07 Август, 2012 09:31 
Аватара пользователя

Зарегистрирован: Суббота, 29 Март, 2008 19:27
Сообщения: 1098
Откуда: Россия, Чебоксары
Илья Ермаков писал(а):
...синтаксическая правильность, соответствие нарисованной схемы графовой грамматике.
"Только программист может дать такой абсолютно точный и столь же бесполезный ответ". :D
А то здесь никто не понимает про синтаксическую правильность, ага.

Вопрос в том, что НАДО автоматически поддерживать эту правильность, и в том, как именно это обеспечить (в том числе в плане свободы пользовтаеля).

И вопрос в том, что силуэт в принципе разрушает синтаксическую правильность, для поддержания которой в этом случае требуются нетривиальные и до сих пор чётко не определённые навороты.

Топологическое преобразование графа из "примитива" в "силуэт" и обратно должно быть однозначным. А этого нет в нынешней форме языка. Поэтому он нарушает самим же собой продекларированные принципы.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 07 Август, 2012 09:38 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 1443
Alexey_Donskoy писал(а):
...
Топологическое преобразование графа из "примитива" в "силуэт" и обратно должно быть однозначным. А этого нет в нынешней форме языка. Поэтому он нарушает самим же собой продекларированные принципы.
Это да... а то описание вот в этом примере - не более, чем литературная зарисовка... :) дальнейший анализ выявил многообразие возможностей перехода... где-то писал об этом...


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Вторник, 07 Август, 2012 14:36 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 631
Откуда: Россия, Орёл
Alexey_Donskoy писал(а):
Топологическое преобразование графа из "примитива" в "силуэт" и обратно должно быть однозначным. А этого нет в нынешней форме языка. Поэтому он нарушает самим же собой продекларированные принципы.


Ну а как Вы будете отображать автоматную логику без силуэта?

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Вторник, 07 Август, 2012 15:23 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 1443
Например, вот так...
Кстати, в импер-части этого примера видно, что многоветочный цикл тоже м.б. (здесь - как "сверхцикл" по цепочке разных состояний)... но Вы имели в виду, полагаю, другое - не разрывать тело обычного цикла (в частности, представляющего одно состояние) на две и более веток.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Вторник, 07 Август, 2012 15:42 
Аватара пользователя

Зарегистрирован: Суббота, 29 Март, 2008 19:27
Сообщения: 1098
Откуда: Россия, Чебоксары
Илья Ермаков писал(а):
Другой вопрос, что пропаганду использования межветочных циклов нужно бы признать неправильной. Т.е. если в программе есть явно выраженный традиционный цикл (а не случай переходов между состояниями), не должен он никогда быть раскиданным между ветками.
О том и речь.
Уф-ф... Не прошло и пяти лет (или уже прошло? :wink: ).


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Вторник, 07 Август, 2012 15:48 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 1443
Чё-то упустил... И.Е. высказывался в пользу разрыва тел циклов между ветками силуэта?..


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Четверг, 09 Август, 2012 13:17 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 5844
Откуда: Москва
Ильченко Эдуард в сообщении viewtopic.php?p=73759#p73759 писал(а):
Хотелось верить в чудо. Что доказательство этой теоремы ведёт и к доказательству (мною не улавливаемому) правильности алгоритма (хоть в какой-то части).
Да, ведет. Не полностью, а в некоторой части. В какой части? В части управляющих операторов. Ведь именно управляющие операторы преобразуются в шампур-схему.

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

ПОЯСНЕНИЕ

В самом деле, что происходит после заполнения икон?
Шампур-схема превращается в алгоритм.

Но! При заполнении икон управляющие операторы не записываются внутри икон.
Они исчезают. Ведь их нигде нет. Они невидимы.

Как это возможно? Это возможно потому, что управляющие операторы превратились в шампур-схему.

Фокус в том, что управляющие операторы НЕ ИСЧЕЗЛИ, а ИЗМЕНИЛИ форму своего бытия.

Они "ушли" из текстовой формы представления процедурных знаний.
И "вошли" в графическую форму, то есть в форму шампур-схемы.

Управляющие операторы полностью сохраняют свои фукции, будучи представленными в графической форме (в виде шампур-схемы).

Можно сказать по-другому. Управляющие операторы инвариантны относительно преобразования "текстовая форма записи — графическая форма записи".

ВЫВОД

Цитата:
Вопрос. Какую практическую ценность имеет строгое математическое доказательство правильности построения шампур-схемы-пустышки для доказательства алгоритма (который появится в будущем посредством заполнения икон)?

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


Последний раз редактировалось Владимир Паронджанов Четверг, 09 Август, 2012 14:08, всего редактировалось 2 раз(а).

Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Четверг, 09 Август, 2012 14:00 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 631
Откуда: Россия, Орёл
Владимир Паронджанов писал(а):
Практическая ценность состоит в том, что управляющие операторы алгоритма, представленные в виде шампур-схемы оказываются безошибочными, гарантированно правильными.[/b]
[/quote]

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

А, например, методы Дейкстры или формальной верификации типа model-checking позволяют убедиться в том, что поведение программы соответствует спецификации требований.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Четверг, 09 Август, 2012 15:18 
Аватара пользователя

Зарегистрирован: Вторник, 04 Октябрь, 2011 17:45
Сообщения: 585
Илья Ермаков писал(а):
Владимир Паронджанов писал(а):
Конструктор обеспечивает то же самое, что синтаксический анализатор обычных языков, но другим способом.


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

Если я правильно понял концепцию ДРАКОН-конструктора, она такова:
1) В каждый момент времени на листе находится правильная ДРАКОН схема.
2) Действия, разрешённые конструктором, приводят к изменённой, но тоже правильной ДРАКОН-схеме.

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

Это хорошая гарантия. Но у неё есть и минусы.
Например:

Пусть есть какая-то ДРАКОН-схема А. Я смотрю на неё, и она мне не нравится. Её нужно изменить
так, чтобы получилась схема Б. Что делать?
1) В идеальном редакторе я должен придумать последовательность шагов, которые приведут схему
из точки А в точку Б. Это тяжёлый умственный труд.
2) В графическом, свободном редакторе думать не надо. Можно просто передвинуть иконы туда, куда нужно.

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Четверг, 09 Август, 2012 17:13 
Аватара пользователя

Зарегистрирован: Суббота, 29 Март, 2008 19:27
Сообщения: 1098
Откуда: Россия, Чебоксары
Степан Митькин писал(а):
Если я правильно понял концепцию ДРАКОН-конструктора, она такова:
1) В каждый момент времени на листе находится правильная ДРАКОН схема.
2) Действия, разрешённые конструктором, приводят к изменённой, но тоже правильной ДРАКОН-схеме.
Это не концепция ДРАКОН-конструктора, а транзакция редактирования, до и после которой схема должна находиться в целостном (и правильном) состоянии.

Степан Митькин писал(а):
1) В идеальном редакторе я должен придумать последовательность шагов, которые приведут схему из точки А в точку Б. Это тяжёлый умственный труд.
По моим оценкам, в среде Тышова до 70% ресурсов отнимает :)

Степан Митькин писал(а):
2) В графическом, свободном редакторе думать не надо. Можно просто передвинуть иконы туда, куда нужно.
Если при этом разрываются связи линий с блоками (как было в тех версиях, которые я смотрел), то это ХУЖЕ текстового редактора (не говоря уж о среде Тышова). В тексте хотя бы порядок сохраняется всегда, а тут периодически восстанавливать надо.

Выводы:
1) если редактор не поддерживает транзакции редактирования, которые не могут быть завершены с нарушением синтаксиса - это плохой редактор;
2) если редактор поддерживает транзакции редактирования, которые обеспечивают прозрачное для пользователя сохранение (преобразование) семантики, это очень хороший редактор.

Вашу среду пока можно дисквалифицировать по п.1 - нарушить синтаксис легко простым перетаскиванием элементов.
Среда Тышова удовлетворяет п.1, но не п.2.

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

П.2 частично выполняется средой Тышова. Например, рокировка в развилке удобно изменяет форму представления, сохраняя семантику. Но в чуть более сложных случаях, чем пара полностью вложенных развилок, подобное преобразование становится невозможным (или, по крайней мере, требующим пересечений).

Вопрос, поднятый Эдуардом (о переносе петли цикла), вообще говоря, относится к п.2.
Человек, желающий перенести петлю, может сделать это тремя путями:
а) внести кусок кода в тело цикла (или вынести оттуда);
б) переместить петлю;
в) всё разобрать и собрать заново (как в Вашей среде со свободным рисованием) :wink:

Очевидно, что вариант (в) рассматривать нет смысла, а варианты (а) и (б) топологически эквивалентны. Но тут я соглашусь с Паронджановым, что методически верно будет ставить задачу именно в формулировке (а) :D
Соответственно, и редактор должен если не навязывать, то поощрять вариант (а)...


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Четверг, 09 Август, 2012 18:04 

Зарегистрирован: Воскресенье, 24 Февраль, 2008 15:32
Сообщения: 5844
Откуда: Москва
Илья Ермаков писал(а):
Владимир Паронджанов писал(а):
Практическая ценность состоит в том, что управляющие операторы алгоритма, представленные в виде шампур-схемы оказываются безошибочными, гарантированно правильными.[/b]

Владимир Даниелович, синтаксически безошибочными, но не семантически.

Уважаемый Илья Евгеньевич!

Вы правы. И я с Вами согласен. Наши мысли во многом совпадают:
Цитата:
Дракон-конструктор осуществляет 100%-е автоматическое доказательство правильности шампур-схем, гарантируя принципиальную невозможность ошибок визуального синтаксиса.

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

1. В виде надписей да и нет возле выходов иконы вопрос.
Можно перепутать да и нет местами? Да, можно. Но вероятность этого невелика.

2. При записи условий внутри иконы вопрос.
При записи условий тоже можно ошибиться. Но и здесь для защиты от ошибок есть специальные средства.

        — Понятие "каноническая дракон-схема", полностью исключающая связки И, ИЛИ, НЕ.

        — Приведение дракон-схемы к каноническому виду.

        — Понятие "стандартная дракон-схема".

        — Понятие "нестандартная дракон-схема" и др.

Перечисленные средства подробно описаны в книге "Учись..." в главе 11
Цитата:
Глава 11. Логические формулы, используемые в алгоритмах ...153—183

ВЫВОДЫ

1. Для уменьшения вероятности ошибок в управляющих операторах в языке ДРАКОН используются синтаксические и семантические средства.

2. Синтаксические средства реализованы в дракон-конструкторе, который гарантирует невозможность ошибок визуального синтаксиса.

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

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


Последний раз редактировалось Владимир Паронджанов Пятница, 10 Август, 2012 10:44, всего редактировалось 3 раз(а).

Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Философия ДРАКОН-конструктора
СообщениеДобавлено: Пятница, 10 Август, 2012 08:04 

Зарегистрирован: Воскресенье, 01 Ноябрь, 2009 05:13
Сообщения: 1443
Владимир Даниелович, да ведь Илья Евгеньевич не об этом говорит. А о том, что программа д.б. корректна как целое - т.е. не только в импер-структурной части.
Что с т.зр. получения требуемого от программы (а равно - информатизованной инструкции для "человека как машины") результата (допустимого соответствия множества вариантов использования на множестве вариаций исходных данных - притом коректно использующего ресурсы исполнителя) даёт соответствие "слепыша" правилам шампур-организации, если текст для заполнения "слепыша" (реально превращающий его в программу/инфор-инструкцию) сформулирован неверно?.. Например, какие-то выражения (т.е. импер-атрибутивная часть)... и/или атрибуция типов... я уже не говорю о типовой структуре, которую также на импер-"слепыше" не покажешь - тоже только текстом описывать, как Ярослав делает?..
Сама по себе - ничего не даёт. Только как часть целостного представления сочинителя о задаче в расчёте на принятого исполнителя (архитектуру машинной платформы, квалификацию человека).

Теперь о синтаксической правильности для части целого (в данном случае - импер-структурной). Реализовали мы построение схем для этой части - и что? Алексей ведь правильно о тексте вспомнил - потому что так можно понять, что это даёт. А вот что - гарантию, что структура ключевых слов из той самой "тщательно обосновываемой коллекции" (напр. Дейкстрой для структурного программирования) будет всегда корректной по определению текстового инфор-языка, взятого для реализации. Скажем, какого-то ТЯП... или стандарта псевдокода. Т.е. в тексте, изоморфном схеме (а он д.б. всегда) эти слова будут образовывать корректные конструкции (проходимые для синтразбора).
При этом остальное содержание целого (программы, инфор-инструкции) с т.зр. "слепышей" нужно считать ведь некими полями, параметризующими импер-структуру до целого. А вот чего там будет в этих полях - зависит уже от реализации других частей синтаксиса... И от того, что сформулирует сочинитель. А редактор, "заточенный" только на доказательность в импер-структурной части, эти остальные части никак не проверит... и корректность исполнения программы/инфор-инструкции как целого не установит...
Притом заметим - синтаксис этих остальных частей м.б. ох каким разным... в своих РБНФ-определениях я ведь дал возможные варианты только примерно.
Не говоря о том, что есть уровни семантики и способы их выражения (качественный - "родной", математический - напр., функциональный, информатический - высоко/низкоуровневый)... И им будут сотвествовать разные допустимые синтаксисы и в части импер-структур (скажем, на джамп-асме есть явные БП - а на ЯВУ м.б. и нет... зато ретурны м.б. - а выше в математической схеме порядок исполнения вообще иначе выражаться может)...
Короче, для каждого конкретного языка правильность придётся уточнять. И будет у нас целое семейство стандартов на языки импер-"слепышей"...

Т.е. мало сочинителю, чтобы редактор не дал ему нарисовать неправильную схему. Думать над семантикой целого и над её соответствием задаче всё равно надо...
Замечу - и когда мы реализуем схемы для остальных частей целого (декларативной и активностной) - это останется в силе.
В чём же плюс перехода от текста к графам для структурных частей? В том, о чём Вы не устаёте говорить - думать сочинителю часто оказывается легче... А формально доказывать правильность всё равно иначе надо - сочетанием тестирования и верификации... возможные методы И.Е. тже упомянул...


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 81 ]  На страницу Пред.  1, 2, 3, 4, 5  След.

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


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

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


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

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