محيطي براي توليد برنامه از توصيف صوري

The use of traditional software development methods is subject to problems such as lack of confidence in the correctness of the final product. The application of formal methods to the specification of software systems is expected to increase the level of this confidence. However, the gap between the two phases of program specification and program development causes this confidence in correctness to be degraded yet again during the transition from the specification to the actual program. A number of methods for developing programs from their formal specifications have been proposed, one of which is the method of deriving programs from the correctness proofs of formal specifications. In this paper, an environment for developing reliable programs from formal specifications is introduced. The formal specifications arc written in a constructive version of the Z notation, called CZ. An automatic translation tool has been designed and implemented that can translate the correctness proofs of such a specfication into the corresponding proofs in Martin-Lof theory of types. Finally, the program is derived from the translated correctness proofs.