Верификация и синтез программ сложения на базе правил корректности операторов

Дедуктивная верификация и синтез программ двоичного сложения проводятся на базе системы правил доказательства корректности для операторов языка предикатного программирования $P$. В работе представлены ключевые фрагменты процесса верификации и синтеза программ сумматоров. Условия корректности программ транслировались на язык спецификаций системы автоматического доказательства PVS. Доказательство на PVS оказалось на порядок более трудоемким процессом по сравнению с обычным программированием. Однако в режиме синтеза построение теорий и доказательство на PVS проще и быстрее по сравнению с верификацией.