DRAKON.SU

Текущее время: Вторник, 19 Март, 2024 12:19

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




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

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

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

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

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

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


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

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

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


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 01 Сентябрь, 2017 06:29 

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


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

Зарегистрирован: Воскресенье, 09 Март, 2008 22:38
Сообщения: 341
Владимир Шелехов писал(а):
для реальных программ автоматический программный синтез практически невозможен

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

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

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


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

Зарегистрирован: Среда, 09 Ноябрь, 2016 00:33
Сообщения: 122
Откуда: Tallinn
коллега по работе будучи учеником Тыугу сделал опенсорсный проект, может кому будет интересно https://cocovila.github.io/
вот видео https://www.youtube.com/watch?v=pHx4yQTHMPI


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Суббота, 23 Сентябрь, 2017 02:15 

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

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


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

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


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

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


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

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