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

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

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

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

Прежде всего нужен метод доказательства корректности программы. Есть классический метод Хоара для императивных программ. У меня свой метод. На его базе построена система правил, применяемая при доказательстве корректности программы. Система правил расширена на случай рекурсивных вызовов с использованием меры. В основе этих правил -- классическая техника доказательства по индукции.

Доказывать корректность программы можно вручную или автоматически через инструмент автоматического доказательства. Не принципиально. Однако вручную можно ошибиться и пропустить ошибку в программе.

Статьи с доказательствами вручную закончились лет 15 назад. Вот одна из классических работ.

Метод дедуктивной верификации предикатных программ описывается в статье М.С.Чушкина. Примеры можно найти в препринте.

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

Спасибо за ответ. Понял, что доказательство основывается на математической индукции.

Видел публикацию: http://www.cs.utexas.edu/users/moore/pu ... -2014a.pdf
Как считаете, она как-нибудь связана с темой предикатного программирования?

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

Rifat писал(а):
Видел публикацию: http://www.cs.utexas.edu/users/moore/pu ... -2014a.pdf
Как считаете, она как-нибудь связана с темой предикатного программирования?
Не связана.
Это история реализации математической индукции в пруверах. Старой формации.
Про современные пруверы: PVS, Coq, Hol, ... -- ничего.
А там много интересного.
Например, в PVS поддерживается ординальная индукция.

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

Владимир Шелехов писал(а):
для реальных программ автоматический программный синтез практически невозможен

Владимир Иванович, это - весьма сильное утверждение.

Вот система ПРИЗ с ее концептуальным программированием - она синтезировала "реальные" программы али как?

Кстати, обращаем внимание на диссертацию 2011 года.

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

коллега по работе будучи учеником Тыугу сделал опенсорсный проект, может кому будет интересно https://cocovila.github.io/
вот видео https://www.youtube.com/watch?v=pHx4yQTHMPI

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

Игорь Мазница писал(а):
коллега по работе будучи учеником Тыугу сделал опенсорсный проект, может кому будет интересно https://cocovila.github.io/
вот видео https://www.youtube.com/watch?v=pHx4yQTHMPI

Очень интересно! Спасибо!

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