Interactive Proofs of Programs
S Motty, Theodore S. Norvell · 2010
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 simplified by adding a graphical editor for entry of specifications, 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 theories written in the HOL4/Kananaskis language are presented.