Verification and Synthesis of Effective Programs for Standard Functions under Predicate Programming Technology

V. I. Shelekhov , E-mail: vshel@iis.nsk.su

The technology of development of the effective standard functions isqrt, floor, and ilog2 is described. Correctness of the programs is achieved by application of deductive verification and program synthesis methods. The proof of program correctness conditions is supported by the PVS Verification System.

Keywords: predicate programming, deductive verification, program synthesis, total correctness of program

pp. 14–21