maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-1056Research ArticleОригинальные статьиArticlesВерификация и синтез программ сложения на базе правил корректности операторовVerication and synthesis of addition programs under the rules of statement correctnessШелеховВ. И.ShelekhovV. I.vshel@iis.nsk.suИнститут систем информатики им. А.П. Ершова, г. НовосибирскRussian Federation201020122010174101110Copyright © Шелехов В.И., 20102010Шелехов В.И.Shelekhov V.I.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1056

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

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.

предикатное программированиедедуктивная верификацияпрограммный синтезтотальная корректность программыpredicate programmingdeductive veri cationprogram synthesistotal correctness of programReferencesКарнаухов Н.С., Першин Д.Ю., Шелехов В.И. Язык предикатного программирования P. Новосибирск, 2010. 42 с. (Препр. / ИСИ СО РАН; N 153)Карнаухов Н.С., Першин Д.Ю., Шелехов В.И. Язык предикатного программирования P. Новосибирск, 2010. 42 с. (Препр. / ИСИ СО РАН; N 153)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.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.Шелехов В.И. Модель корректности программ на языке исчисления вычислимых предикатов. Новосибирск, 2007. 50 с. (Препр. / ИСИ СО РАН; N 145).Шелехов В.И. Модель корректности программ на языке исчисления вычислимых предикатов. Новосибирск, 2007. 50 с. (Препр. / ИСИ СО РАН; N 145).Flynn M.J., Oberman S.F. Advanced computer arithmetic design. Wiley, New York. 2001. 344 p. (http://en.wikipedia.org/wiki/Adder_(electronics))Flynn M.J., Oberman S.F. Advanced computer arithmetic design. Wiley, New York. 2001. 344 p. (http://en.wikipedia.org/wiki/Adder_(electronics))Owre S., Rushby J.M., and Shankar N. PVS: A Prototype Verification System // LNCS, 607. 1992. P. 748-752. ( http://pvs.csl.sri.com/)Owre S., Rushby J.M., and Shankar N. PVS: A Prototype Verification System // LNCS, 607. 1992. P. 748-752. ( http://pvs.csl.sri.com/)Sorensen M.H., Urzyczyn P. Lectures on the Curry-Howard Isomorphism // Logic and the Foundations of Mathematics. 2006. Vol. 149. 457 p.Sorensen M.H., Urzyczyn P. Lectures on the Curry-Howard Isomorphism // Logic and the Foundations of Mathematics. 2006. Vol. 149. 457 p.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/)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/)Doran R. W. Variants of an Improved Carry Look-Ahead Adder // IEEE Transactions on Computers. 1988. Vol. 37, No.9. P. 1110-1113.Doran R. W. Variants of an Improved Carry Look-Ahead Adder // IEEE Transactions on Computers. 1988. Vol. 37, No.9. P. 1110-1113.Basin D., DeVille Y., Flener P., Hamfelt A., and Nilsson J. Synthesis of programs in computational logic // LNCS, 3049. P. 30-65, 2004.Basin D., DeVille Y., Flener P., Hamfelt A., and Nilsson J. Synthesis of programs in computational logic // LNCS, 3049. P. 30-65, 2004.Srivastava S., Gulwani S., and Foster J. From Program Verification to Program Synthesis. POPL, 2010. P. 313-326.Srivastava S., Gulwani S., and Foster J. From Program Verification to Program Synthesis. POPL, 2010. P. 313-326.Шелехов В.И. Верификация и синтез эффективных программ стандартных функций floor, isqrt и ilog2 в технологии предикатного программирования // Тр. 12-й межд. конф. "Проблемы управления и моделирования в сложных системах". Самарский научный центр РАН, 2010. С. 622-630.Шелехов В.И. Верификация и синтез эффективных программ стандартных функций floor, isqrt и ilog2 в технологии предикатного программирования // Тр. 12-й межд. конф. "Проблемы управления и моделирования в сложных системах". Самарский научный центр РАН, 2010. С. 622-630.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.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.

The authors declare that there are no conflicts of interest present.