Automatic Algorithm Programming Model Based on the Improved Morgan's Refinement Calculus  

作　　者：ZUO Zhengkang HU Ying HUANG Qing WANG Yuan WANG Changjing 

机构地区：[1]School of Computer Information Engineering,Jiangxi Normal University,Nanchang 330022,Jiangxi,China [2]School of Software,Jiangxi Normal University,Nanchang 330022,Jiangxi,China

出　　处：《Wuhan University Journal of Natural Sciences》2022年第5期405-414,共10页武汉大学学报（自然科学英文版）

基　　金：Supported by the National Natural Science Foundation of China(61862033,61902162);Key Project of Science and Technology Research of Department of Education of Jiangxi Province(GJJ210307);Postgraduate Innovation Fund Project of Education Department of Jiangxi Province(YC2021-S306)。

摘　　要：The automatic algorithm programming model can increase the dependability and efficiency of algorithm program development,including specification generation,program refinement,and formal verification.However,the existing model has two flaws:incompleteness of program refinement and inadequate automation of formal verification.This paper proposes an automatic algorithm programming model based on the improved Morgan’s refinement calculus.It extends the Morgan’s refinement calculus rules and designs the C++generation system for realizing the complete process of refinement.Meanwhile,the automation tools VCG(Verification Condition Generator)and Isabelle are used to improve the automation of formal verification.An example of a stock’s maximum income demonstrates the effectiveness of the proposed model.Furthermore,the proposed model has some relevance for automatic software generation.

关 键 词：automatic algorithm programming model program refinement VCG ISABELLE Morgan’s refinement calculus 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]