Interactive Proofs Of Programs Using HOL


Programs can be treated as mathematical objects and thus proofs of programs are simply mathematical proofs. Software that handles proofs in various areas of mathematics such as HOL4/Kananaskis can therefore be used for verification that programs meet their specifications. User interaction will be simplifiedbyaddingagraphicaleditorforentryofspecifications, programs, and proofs; the editor is coupled to the proof-checker using a client/server interface. This paper describes progress being made in support of the above software design methodology. Demonstrations of some essential proofs and core theorieswritten in the HOL4/Kananaskis language are presented.

Full text as PDF