Towards Semi-Automatic Generation of Provably Correct Algorithmic Programs

The paper gives an overview of a PAR-based Algorithm Design System PADS. PADS provides formal and semi-automatic support for the generation of algorithmic programs as well as loop invariants. It has several extensible built-in libraries that contain strategies and rules for PAR-based algorithm design. To illustrate the use of PADS, an example is given. PADS aims to bring a mechanizable and unified development process which starts from a high-level specification and results in provably correct products, meanwhile enables users with little mathematical knowledge about formal methods to develop algorithmic programs efficiently.