| Issue |
Wuhan Univ. J. Nat. Sci.
Volume 27, Number 5, October 2022
|
|
|---|---|---|
| Page(s) | 405 - 414 | |
| DOI | https://doi.org/10.1051/wujns/2022275405 | |
| Published online | 11 November 2022 | |
Computer Science
CLC number: TP 311
Automatic Algorithm Programming Model Based on the Improved Morgan's Refinement Calculus
1
School of Computer Information Engineering, Jiangxi Normal University, Nanchang 330022, Jiangxi, China
2
School of Software, Jiangxi Normal University, Nanchang 330022, Jiangxi, China
† To whom correspondence should be addressed. E-mail: wcj771006@163.com
Received:
12
December
2021
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.
Key words: automatic algorithm programming model / program refinement / VCG / Isabelle / Morgan's refinement calculus
Biography: ZUO Zhengkang, male, Ph.D., Professor, research direction: software formal methods and generic programming. E-mail: zhengkang2005@iscas.ac.cn
Fundation item: 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) and Postgraduate Innovation Fund Project of Education Department of Jiangxi Province(YC2021-S306)
© Wuhan University 2022
This is an Open Access article distributed under the terms of the Creative Commons Attribution License (https://creativecommons.org/licenses/by/4.0), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.