  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.
