Reusable Problem Domain Theories

One of the main reasons why constructing deductive proofs that programs satisfy their specifications can be very expensive in practice is the absence of reusable problem domain theories. These theories contain functions that define relevant concepts in the application area of the program, and they contain properties that are deduced from these definitions. Presently, the cost of proving programs is highly inflated by the fact that we usually have to build a new problem domain theory for each new application. If we can develop reusable problem domain theories, the cost of specifying and proving programs in actual practice can be greatly reduced. The development of these theories also would have significant benefits for other aspects of computing science. This paper discusses the composition of problem domain theories and their relation to program specification and proof. REUSABLE PROBLEM DOMAIN THEORIES 2 Acknowledgements During its eight year existence, well over 50 people have contr..