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

Полный текст:


Аннотация

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

Об авторе

В. И. Шелехов
Институт систем информатики им. А.П. Ершова, г. Новосибирск
Россия


Список литературы

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.)

Просмотров: 10

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)