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/ |