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 veriﬁcation that programs meet their speciﬁcations. User interaction will be simpliﬁedbyaddingagraphicaleditorforentryofspeciﬁcations, 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.