  These notes outline a formal method for program verification of numerical
computation. It forms the basis of the software package VPC in its initial
phase of development. Much of the style of presentation is in the form of notes
that outline the definitions and rules upon which VPC is based. The initial
motivation of this project was to address some practical issues of computation,
especially of numerically intensive programs that are commonplace in computer
models. The project evolved into a wider area for program construction as
proofs leading to a model of inference in a more general sense. Some basic
results of machine arithmetic are derived as a demonstration of VPC.
