An Approach to Formal Definitions and Proofs of Programming Principles
Jayadev Misra · IEEE Transactions on Software Engineering · 1978
A method for formal description of programming prinicples is presented in this paper. Programming principles, such as sequential search can be defined and proven even in the absence of an application. We represent a principle as a program scheme which has partially interpreted functions in it. The functions must obey certain input constraints. Use of these ideas in program proving is illustrated with examples.