Program Verification of Numerical Computation - Part 2

TL;DR

This paper extends a formal verification method for numerical programs, enhancing its capabilities with disjunctions, non-computability detection, and higher-order constructs, forming the basis for the VPC software.

Contribution

Introduces significant extensions to a formal verification method, including disjunctions, non-computability detection, and higher-order constructs, advancing program verification tools.

Findings

Enhanced verification method with disjunctions

Methods for detecting non-computable programs

Expanded construction rules for higher-order constructs

Abstract

These notes present some extensions of a formal method introduced in an earlier paper. The formal method is designed as a tool for program verification of numerical computation and forms the basis of the software package VPC. Included in the extensions that are presented here are disjunctions and methods for detecting non-computable programs. A more comprehensive list of the construction rules as higher order constructs is also presented.