9410236 Jia The purpose of the proposed research is to develop a feasible and effective approach to software development based on Z formal specifications that is suitable for industrial applications. The goal is to synthesize production-quality code. It does not intend to fully automate the development process, rather to integrate design refinement, program synthesis, software components reuse, and manual development. The proposed approach depends on human engineers to make design decisions through interactive sessions, and it attempts to fully automate the implementation processes. The key components of the proposed approach include design refinement using predicate transformation, refinement of loose specifications, reusing and fine-tuning of generic algorithms and data structures. The proposed project will experimentally apply the proposed approach in industrial environments. Prototypes of supporting tools for design refinement and code synthesis will be developed. ***
