DRAKON.SU

viewtopic.php?f=62&t=5077&p=94602#p94602

Это ответ на вопрос в сообщении viewtopic.php?f=140&p=100105#p100105


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

Посмотрел вашу лекцию по поводу предикатного программирования.
Как я понял, решение приводится при помощи рекурсивных функций.
А также используется понятие "меры", насколько я понял, это аналог ограничивающей функции у циклов.
Я правильно понял?

Похоже на то.

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

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

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

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

Критерий прост: в компиляторе есть поисковые алгоритмы ИИ и машинное обучение? Нет? Добро пожаловать в средние века.

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

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

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

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

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

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

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

Сейчас почитал еще про предикатное программирование.

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

Да, с помощью рекурсивных программ, т.е. рекурсивно определяемых предикатов. Циклов нет.
Верно, мера используется для доказательства того, что программа завершается.

Генеральная классификация выглядит несколько по другому.

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

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

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

Рекурсивные программы отличаются от итеративных тем, что при рекурсии есть неявный стек. В принципе можно использовать явный стек и цикл и получится взаимо-однозначное соответствие с рекурсивными программами. Мне кажется, что это не принципиально использовать ли рекурсивные фукции или циклы.

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

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

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

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

Возьмён умножение матриц.
Цикл Для заменяем на квантор всеобщности (Для Всех).

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

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

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

Рассмотрим сортировку.

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

Чего ж проще? Сравните это хотя бы с пузырьковой сортировкой.
Можно расшифровать понятия "эквивалентная" и "отсортирована".

Опять-таки квантор всеобщности вместо Цикла Для.

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

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

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

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

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

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


Будет!