DRAKON.SU
https://forum.drakon.su/

Дискуссия по формальным методам и инженерии требований
https://forum.drakon.su/viewtopic.php?f=140&t=5581
Страница 3 из 4

Автор:  LKom [ Среда, 27 Январь, 2016 14:01 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

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

Автор:  Владимир Шелехов [ Четверг, 28 Январь, 2016 09:59 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

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 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

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

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

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

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

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

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

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

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

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

Автор:  Rifat [ Понедельник, 21 Август, 2017 17:06 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

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

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

Автор:  Владимир Паронджанов [ Понедельник, 21 Август, 2017 21:58 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

Владимир Шелехов писал(а):
Императивное программирование должно было остаться в прошлом.
Прошло сорок лет, но этого не произошло.
Реальная история сделала другой зигзаг.

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

Автор:  Степан Митькин [ Вторник, 22 Август, 2017 10:40 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

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

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

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

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

Автор:  Владимир Шелехов [ Вторник, 22 Август, 2017 16:08 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

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

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

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

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

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

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

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

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

Автор:  Rifat [ Вторник, 22 Август, 2017 17:06 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

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

Автор:  Степан Митькин [ Среда, 23 Август, 2017 10:14 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

Rifat писал(а):
Как я понял, решение приводится при помощи рекурсивных функций.

Похоже на то.

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

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

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

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

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

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

Автор:  Rifat [ Среда, 23 Август, 2017 10:27 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

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

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

Автор:  Степан Митькин [ Среда, 23 Август, 2017 13:15 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

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


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

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

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

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

Автор:  Rifat [ Среда, 23 Август, 2017 13:20 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

Сейчас почитал еще про предикатное программирование.
Цитата:
Предикатная программа есть набор рекурсивных определений предикатов, среди которых могут находиться описания типов и глобальных переменных.

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

Автор:  Владимир Шелехов [ Четверг, 24 Август, 2017 14:47 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

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

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

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

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

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

Автор:  Rifat [ Четверг, 24 Август, 2017 18:34 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

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

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

Автор:  Владимир Шелехов [ Пятница, 25 Август, 2017 14:38 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

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

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

Автор:  Степан Митькин [ Среда, 30 Август, 2017 09:53 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

Владимир Шелехов писал(а):
Еще круче автоматический программный синтез.

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

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

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

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

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

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

Автор:  Степан Митькин [ Среда, 30 Август, 2017 10:03 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

Рассмотрим сортировку.
Вложение:
sort.png
sort.png [ 4.41 КБ | Просмотров: 12221 ]

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

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

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

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

Автор:  Владимир Шелехов [ Четверг, 31 Август, 2017 07:41 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

Степан Митькин писал(а):
Владимир Шелехов писал(а):
Еще круче автоматический программный синтез.

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

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

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

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

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

Автор:  Rifat [ Четверг, 31 Август, 2017 11:06 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

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

Автор:  Степан Митькин [ Четверг, 31 Август, 2017 11:57 ]
Заголовок сообщения:  Re: Дискуссия по формальным методам и инженерии требований

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


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

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

Будет!

Страница 3 из 4 Часовой пояс: UTC + 3 часа
Powered by phpBB® Forum Software © phpBB Group
https://www.phpbb.com/