Verication and synthesis of addition programs under the rules of statement correctness
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 Li...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2010-12-01
|
| Series: | Modelirovanie i Analiz Informacionnyh Sistem |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/1056 |
| Summary: | 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. |
|---|---|
| ISSN: | 1818-1015 2313-5417 |