УДК: 004.415.52

Верификация и синтез эффективных программ стандартных функций в технологии предикатного программирования

В.И. Шелехов, канд. техн. наук, зав. лаб., Институт систем информатики им. А.П. Ершова СО РАН, г. Новосибирск, E-mail: vshel@iis.nsk.su

Описывается технология построения эффективных программ стандартных функций isqrt, floor и, ilog2. Корректность программ обеспечивается дедуктивной верификацией и программным синтезом. Условия корректности программ доказываются с помощью системы автоматического доказательства PVS.

Ключевые слова: предикатное программирование, дедуктивная верификация, программный синтез, тотальная корректность программы

Стр. 14–21