Verification and synthesis of addition programs under the rules of correctness of statements |
| |
Authors: | V I Shelekhov |
| |
Affiliation: | 1.Institute of Informatics Systems, Siberian Branch,Russian Academy of Sciences,Novosibirsk,Russia |
| |
Abstract: | Deductive verification and synthesis of binary addition programs are carried out on the base of the rules of proving the correctness
for statements of the predicate programming language P. The paper presents key fragments of verification 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 specification language of the PVS verification system. The proof is found to be a tedious procedure as compared with
the ordinary programming. However, for program synthesis, the development of theories and proofs on PVS are easier and faster
than for program verification. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|