Haihe Shi, Chinese Academy of Sciences, China; Graduate University of Chinese Academy of Sciences, China; Jiangxi Normal University, China
Jinyun Xue, Chinese Academy of Sciences, China; Jiangxi Normal University, China
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.
Citation:
Haihe Shi, Jinyun Xue, "Towards Semi-Automatic Generation of Provably Correct Algorithmic Programs," snpd, vol. 3, pp.952-957, Eighth ACIS International Conference on Software Engineering, Artificial Intelligence, Networking, and Parallel/Distributed Computing (SNPD 2007), 2007