Verication and synthesis of addition programs under the rules of statement correctness
Abstract
Deductive verication and synthesis of binary addition programs are performed on
the base of the rules of program correctness for statements of the predicate programming
P language. The paper presents the sketch of verication and synthesis of the programs
for the Ripple carry, Carry look-ahead and Ling adders. The correctness conditions of the
programs were translated into the specication language of the PVS verication system.
The time needed to prove the program correctness conditions in the PVS is more than the
time of the ordinary programming by a factor of 10. However, for program synthesis,
development of PVS theories and proofs are easier and faster than that for program
verication.
the base of the rules of program correctness for statements of the predicate programming
P language. The paper presents the sketch of verication and synthesis of the programs
for the Ripple carry, Carry look-ahead and Ling adders. The correctness conditions of the
programs were translated into the specication language of the PVS verication system.
The time needed to prove the program correctness conditions in the PVS is more than the
time of the ordinary programming by a factor of 10. However, for program synthesis,
development of PVS theories and proofs are easier and faster than that for program
verication.
About the Author
V. I. Shelekhov
Институт систем информатики им. А.П. Ершова, г. Новосибирск
Russian Federation
Russian Federation
References
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.
Review
For citations:
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.)
Views:
580
Email this article 