Верификация и синтез программ сложения на базе правил корректности операторов
Аннотация
Дедуктивная верификация и синтез программ двоичного сложения проводятся на базе системы правил доказательства корректности для операторов языка предикатного программирования P. В работе представлены ключевые фрагменты процесса верификации и синтеза программ сумматоров. Условия корректности программ транслировались на язык спецификаций системы автоматического доказательства PVS. Доказательство на PVS оказалось на порядок более трудоемким процессом по сравнению с обычным программированием. Однако в режиме синтеза построение теорий и доказательство на PVS проще и быстрее по сравнению с верификацией.
Ключевые слова
предикатное программирование,
дедуктивная верификация,
программный синтез,
тотальная корректность программы
MSC2020: 004.415.52
Список литературы
1. Карнаухов Н.С., Першин Д.Ю., Шелехов В.И. Язык предикатного программирования P. Новосибирск, 2010. 42 с. (Препр. / ИСИ СО РАН; N 153)
2. Shelekhov V. The language of calculus of computable predicates as a minimal kernel for functional languages // BULLETIN of the Novosibirsk Computing Center. Series: Computer Science. IIS Special Issue. 29(2009). 2009. P. 107-117.
3. Шелехов В.И. Модель корректности программ на языке исчисления вычислимых предикатов. Новосибирск, 2007. 50 с. (Препр. / ИСИ СО РАН; N 145).
4. Flynn M.J., Oberman S.F. Advanced computer arithmetic design. Wiley, New York. 2001. 344 p. (http://en.wikipedia.org/wiki/Adder_(electronics))
5. Owre S., Rushby J.M., and Shankar N. PVS: A Prototype Verification System // LNCS, 607. 1992. P. 748-752. ( http://pvs.csl.sri.com/)
6. Sorensen M.H., Urzyczyn P. Lectures on the Curry-Howard Isomorphism // Logic and the Foundations of Mathematics. 2006. Vol. 149. 457 p.
7. Hehner E.C.R. A Practical Theory of Programming, second edition // ON M5S 2E4, University of Toronto. 2004. 242p. (http://www.cs.toronto.edu/ hehner/aPToP/)
8. Doran R. W. Variants of an Improved Carry Look-Ahead Adder // IEEE Transactions on Computers. 1988. Vol. 37, No.9. P. 1110-1113.
9. Basin D., DeVille Y., Flener P., Hamfelt A., and Nilsson J. Synthesis of programs in computational logic // LNCS, 3049. P. 30-65, 2004.
10. Srivastava S., Gulwani S., and Foster J. From Program Verification to Program Synthesis. POPL, 2010. P. 313-326.
11. Шелехов В.И. Верификация и синтез эффективных программ стандартных функций floor, isqrt и ilog2 в технологии предикатного программирования // Тр. 12-й межд. конф. "Проблемы управления и моделирования в сложных системах". Самарский научный центр РАН, 2010. С. 622-630.
12. Kapur D., Subramaniam M. Mechanical verification of adder circuits using Rewrite Rule Laboratory // Formal Methods in System Design. 1998. Vol. 13, No. 2. P. 127- 158.
Рецензия
Для цитирования:
Шелехов В.И. Верификация и синтез программ сложения на базе правил корректности операторов. Моделирование и анализ информационных систем. 2010;17(4):101-110.
For citation:
Shelekhov V.I. Verication and synthesis of addition programs under the rules of statement correctness. Modeling and Analysis of Information Systems. 2010;17(4):101-110. (In Russ.)
Просмотров:
579
Послать статью по эл. почте 