Generating Algorithms plus Loop Invariants by Formal Derivation

We advocate a mechanical derivation approach for developing provably correct algorithmic programs. The paper presents our new formal methods and techniques for generating algorithms plus loop invariants. Through our methods and techniques, the ideas behind MergeSort algorithm is revealed naturally from a formal specification, and then its loop invariant and nonrecursive algorithmic solution are generated mechanically. Furthermore, instead of fresh formal derivation, the Insertion Sort is easily achieved based on the derivation of MergeSort. By means of our tools their executable language programs can be generated automatically. Therefore mathematical knowledge required by formal development process is reduced substantially and the confidence in the resultant code is increased.