DRAKON.SU

Текущее время: Суббота, 26 Май, 2018 05:16

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




Начать новую тему Ответить на тему  [ Сообщений: 66 ]  На страницу Пред.  1, 2, 3, 4  След.
Автор Сообщение
СообщениеДобавлено: Среда, 27 Январь, 2016 14:01 

Зарегистрирован: Среда, 07 Январь, 2015 14:53
Сообщения: 715
http://forum.oberoncore.ru/viewtopic.php?p=94593#p94593
http://forum.oberoncore.ru/viewtopic.php?p=94595#p94595
Владимир Паронджанов писал(а):
Цитата:
Как дела с разработкой редактора у Владимира Шелехова, сообщалось, что к разработке привлекается и Виктор Касьянов.
Об этом лучше спросить у Владимира Шелехова.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 28 Январь, 2016 09:59 

Зарегистрирован: Вторник, 22 Сентябрь, 2015 20:43
Сообщения: 74
LKom писал(а):
http://forum.oberoncore.ru/viewtopic.php?p=94593#p94593
http://forum.oberoncore.ru/viewtopic.php?p=94595#p94595
Владимир Паронджанов писал(а):
Цитата:
Как дела с разработкой редактора у Владимира Шелехова, сообщалось, что к разработке привлекается и Виктор Касьянов.
Об этом лучше спросить у Владимира Шелехова.
viewtopic.php?f=62&t=5077&p=94602#p94602


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Понедельник, 21 Август, 2017 15:35 

Зарегистрирован: Вторник, 22 Сентябрь, 2015 20:43
Сообщения: 74
Это ответ на вопрос в сообщении viewtopic.php?f=140&p=100105#p100105

Rifat писал(а):
Универсальный космический язык (УКЯ) вы во сне увидели?

Наяву. Размышлял, как должно быть устроено программирование.
Перед этим понял, что структурное программирование -- это не решение.
Семь раз скрупулезно прочитал "Заметки о структурном программировании" в надежде изъять оттуда позитивное решение. Его не оказалось.

Я был немногим из счастливцев, кто узнал о структурном программировании от самого Дейкстры в кабинете Андрея Петровича Ершова.

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

В последующие три года, прикладывая все свои силы и способности,
я пытался вытащить увиденное.
Свои рукописи с новым подходом к программированию я приносил А.П. Ершову.
Он меня пинал. Конечно, вежливо и корректно.
Тогда мне недоставало квалификации.

Через три года я был окончательно истощен и понял, что нужно сделать перерыв.
Перерыв оказался в 25 лет.

Сейчас это предикатное программирование. Более 30 публикаций.
Часть видеокурса по формальным методам.

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Понедельник, 21 Август, 2017 17:06 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 208
Откуда: Казань
Владимир Шелехов писал(а):
Перед этим понял, что структурное программирование -- это не решение.
Семь раз скрупулезно прочитал "Заметки о структурном программировании" в надежде изъять оттуда позитивное решение. Его не оказалось.

Расскажите, пожалуйста, почему структурное программирование - это не решение?
Какие у структурного программирования есть недостатки по сравнению с предикатным программированием?


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Понедельник, 21 Август, 2017 21:58 

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

Желательно пояснить, что имеется в виду.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 22 Август, 2017 10:40 
Аватара пользователя

Зарегистрирован: Вторник, 04 Октябрь, 2011 17:45
Сообщения: 458
Владимир Шелехов писал(а):
В расслаблении, спокойно размышляя о правильном устройстве программирования,
я всего на один миг получил кадр с исчерпывающим ответом.

Понятно. Медитация, астрал и зелёные человечки. :D

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

Более того, данный кадр в той презентации был не один.
Я подсмотрел ещё два.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 22 Август, 2017 16:08 

Зарегистрирован: Вторник, 22 Сентябрь, 2015 20:43
Сообщения: 74
Rifat писал(а):
Владимир Шелехов писал(а):
Перед этим понял, что структурное программирование -- это не решение.
Семь раз скрупулезно прочитал "Заметки о структурном программировании" в надежде изъять оттуда позитивное решение. Его не оказалось.

Расскажите, пожалуйста, почему структурное программирование - это не решение?

Структурное программирование объявляет оператор goto опасным и предлагает использовать только правильные операторы: последовательный, условный и цикл while. Больше ничего в структурном программировании по сути нет. Все остальное -- пустые декларации и спекуляции.

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

Структурное программирование - это религия. Она работает как религия.

Это очень коротко. Развернутый анализ будет позже. Есть и вред от структурного программирования.

Rifat писал(а):
Какие у структурного программирования есть недостатки по сравнению с предикатным программированием?

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 22 Август, 2017 17:06 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 208
Откуда: Казань
Посмотрел вашу лекцию по поводу предикатного программирования.
Как я понял, решение приводится при помощи рекурсивных функций.
А также используется понятие "меры", насколько я понял, это аналог ограничивающей функции у циклов.
Я правильно понял?


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 23 Август, 2017 10:14 
Аватара пользователя

Зарегистрирован: Вторник, 04 Октябрь, 2011 17:45
Сообщения: 458
Rifat писал(а):
Как я понял, решение приводится при помощи рекурсивных функций.

Похоже на то.

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

Напоминаю, что есть только 2 парадигмы программирования: ручное и (полу)автоматическое.

1. Объектно-ориентированное, функциональное, процедурное, структурное программирование есть суть ручное программирование. Что это означает? Это означает, что программист берёт за ручку компьютер и ведёт его по каждому шагу программы. Все хитросплетения, каждый узелок программы программист плетёт своими ручками и близорукими глазками.
Транспортная аналогия — велосипед. Движение за счёт энергии тела человека.

2. При (полу)автоматическом программировании человек ставит задачу — как программа должна работать. Далее инструментальные средства (с человеческой помощью) строят программу.
Транспортная аналогия — грузовик. Движение за счёт энергии двигателя.

Критерий прост: в компиляторе есть поисковые алгоритмы ИИ и машинное обучение? Нет? Добро пожаловать в средние века.
Вложение:
20170823090939.png
20170823090939.png [ 45.32 КБ | Просмотров: 3155 ]

Предикатное программирование Шелехова — это ручное программирование, насколько можно понять.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 23 Август, 2017 10:27 

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

Вопрос же в том, почему предикатное программирование лучше, чем структурное программирование?


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 23 Август, 2017 13:15 
Аватара пользователя

Зарегистрирован: Вторник, 04 Октябрь, 2011 17:45
Сообщения: 458
Rifat писал(а):
Вопрос же в том, почему предикатное программирование лучше, чем структурное программирование?


Попробую ответить за Владимира Ивановича.

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

2. Запрет на циклы. Рекурсия вместо циклов.
- Верификатору легче проверять.
- Читателю легче понимать (лично я с этим не согласен, но многие разделяют эту точку зрения).

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 23 Август, 2017 13:20 

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

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 24 Август, 2017 14:47 

Зарегистрирован: Вторник, 22 Сентябрь, 2015 20:43
Сообщения: 74
Rifat писал(а):
Посмотрел вашу лекцию по поводу предикатного программирования.
Как я понял, решение приводится при помощи рекурсивных функций.
Да, с помощью рекурсивных программ, т.е. рекурсивно определяемых предикатов. Циклов нет.
Rifat писал(а):
А также используется понятие "меры", насколько я понял, это аналог ограничивающей функции у циклов. Я правильно понял?
Верно, мера используется для доказательства того, что программа завершается.

Степан Митькин писал(а):
К сожалению, принципиальных отличий предикатного программирования от привычного программирования нет.
Да, дополнительные возможности автоматической проверки правильности — это хорошо.
В остальном же программист пишет программу вручную, как и в средние века.
Напоминаю, что есть только 2 парадигмы программирования: ручное и (полу)автоматическое.
Генеральная классификация выглядит несколько по другому.

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

Императивное, функциональное и примыкающее к ним предикатное программирование по другую сторону от водораздела с логическим программированием. Тут программа исполняется явно в соответствии с правилами языка программирования. Функциональная программа -- это функция. Предикатная программа -- предикат, логическая формула, преобразованная к привычному программному виду. Предикатное программирование существенно отличается от функционального, а они вместе -- от логического с одной стороны и от императивного, с другой. Говорить, что одно программирование -- автоматическое, а другое -- ручное, не совсем корректно. Сравнение обычно проводят по трудоемкости, эффективности, надежности, ...

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 24 Август, 2017 18:34 

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

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 25 Август, 2017 14:38 

Зарегистрирован: Вторник, 22 Сентябрь, 2015 20:43
Сообщения: 74
Rifat писал(а):
Рекурсивные программы отличаются от итеративных тем, что при рекурсии есть неявный стек. В принципе можно использовать явный стек и цикл и получится взаимо-однозначное соответствие с рекурсивными программами. Мне кажется, что это не принципиально использовать ли рекурсивные функции или циклы.

Вашим способом рекурсивные программы к циклам не сводятся.
Хвостовая рекурсия сводится к циклу. Преобразование рекурсии в цикл показано в моей лекции 4.2. Если посмотрите простые приведенные там примеры, то почувствуете, что исходная рекурсивная программа существенно отличается от трансформированной программы с циклами. Итоговая программа сложнее.
Rifat писал(а):
Как я еще заметил, при описании поведения рекурсивных функций, у вас используется аксиоматическое описание, как у абстрактных типов данных. То есть по сути ваш метод я бы определил как предикаты первого порядка + аксиомы функций. И как мне кажется данный подход он применим и к обычным императивным программам и к структурному программированию. Как минимум он им не противоречит.
Не аксиоматическое описание, а формальная операционная семантика ядра -- языка P0, ориентированная исключительно на предикатное программирование и не на что другое. Логика заведомо не первого порядка, поскольку предикатные программы можно подставлять параметрами. В частности, массивы -- объекты логики второго порядка.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 30 Август, 2017 09:53 
Аватара пользователя

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

Речь идёт об этом! Синтез рулит. Всё остальное - жалкое зрелище.
Владимир Шелехов писал(а):
Написать спецификацию в виде предусловия и постусловия сложнее, чем саму программу.

Не будем сгущать краски.
Почему бы не применить ДРАКОН для логической спецификации?

Возьмён умножение матриц.
Цикл Для заменяем на квантор всеобщности (Для Всех).
Вложение:
multiply_matrixes.png
multiply_matrixes.png [ 9.19 КБ | Просмотров: 3007 ]

Это программа частично императивная, частично декларативная.

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

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


Последний раз редактировалось Степан Митькин Среда, 30 Август, 2017 10:04, всего редактировалось 1 раз.

Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 30 Август, 2017 10:03 
Аватара пользователя

Зарегистрирован: Вторник, 04 Октябрь, 2011 17:45
Сообщения: 458
Рассмотрим сортировку.
Вложение:
sort.png
sort.png [ 4.41 КБ | Просмотров: 3007 ]

Эта ДРАКОН-схема говорит: сгенерировать выходную последовательность, которая:
1. эквивалентна входной (содержит те же элементы)
2. отсортирована

Чего ж проще? Сравните это хотя бы с пузырьковой сортировкой.
Можно расшифровать понятия "эквивалентная" и "отсортирована".
Вложение:
equivalent.png
equivalent.png [ 6.29 КБ | Просмотров: 3007 ]

Опять-таки квантор всеобщности вместо Цикла Для.
Вложение:
sorted.png
sorted.png [ 7.72 КБ | Просмотров: 3007 ]

Здесь икона Вопрос применяется для обозначения импликации.
не последний элемент -> следующий элемент не меньше данного


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 31 Август, 2017 07:41 

Зарегистрирован: Вторник, 22 Сентябрь, 2015 20:43
Сообщения: 74
Степан Митькин писал(а):
Владимир Шелехов писал(а):
Еще круче автоматический программный синтез.

Речь идёт об этом! Синтез рулит. Всё остальное - жалкое зрелище.

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

Не будем сгущать краски.
Почему бы не применить ДРАКОН для логической спецификации?
Возьмём умножение матриц. ......... Рассмотрим сортировку. .............

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

У Вас нет опыта формальной спецификации.
Посмотрите, как следует проводить спецификацию сортировки.
Есть еще практическое занятие по формальной спецификации.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 31 Август, 2017 11:06 

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 31 Август, 2017 11:57 
Аватара пользователя

Зарегистрирован: Вторник, 04 Октябрь, 2011 17:45
Сообщения: 458
Владимир Шелехов писал(а):
До сих пор никто не предлагал графический язык для предусловий и постусловий.
...
Он не строгий. Не формальный и не будет воспринят системой дедуктивной верификации.
Интуитивно понятный только Вам. А у остальных будет вызывать вопросы.


Открыл отдельное обсуждение по данному вопросу:
viewtopic.php?f=147&t=6062

Владимир Шелехов писал(а):
У Вас нет опыта формальной спецификации.

Будет!


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

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


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

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


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

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