We advocate an automated refinement approach to developing programs and their proofs. The approach is partially embodied in the Specware system [6] which has found industrial and government applications. Our view is that the future of software engineering lies in the tight integration of synthesis and analysis processes.
展开▼
