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. Email: 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. Email: 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(YC2021S306)
© 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.
0 Introduction
The development of reliable software has become a critical point on which we should concentrate, particularly for systems with high safety requirements, such as aerospace control systems and medical equipment systems. Even minor errors in these systems can result in massive losses^{[1]}.
Formal methods are mathematically based techniques for specifying, developing, and testing computer software and hardware systems. Their mathematical basis is the formal logic systems consisting of formal languages, semantics, and proof systems. Formal methods are increasingly being used with appropriate levels of rigor at various stages of a computing system's lifecycle. It contributes significantly to reliability and security of software^{[24]}.
Algorithm program correctness is the key to software security. However, programmers often write code intuitively. They hope that if there are small misjudgements, those errors will be exposed in the test. The algorithm obtained in this way is very errorprone. It may cause some hidden issues with software security^{[5]}. Automatic algorithm programming model has the potential to improve the reliability and efficiency of algorithm program development.
Automatic algorithm programming model consists of three core processes: specification generation, program refinement, and formal verification. Among the three processes, specification generation uses formal methods to describe user requirements; program refinement turns a specification into an executable program by gradually lowering the level of abstraction; and formal verification verifies the correctness of abstract programs generated during program refinement.
The process of specification generation is relatively simple. As a result, in the following, we would introduce a variety of automatic algorithm programming models based on Dijkstra's weakest precondition method^{[68]}, Morgan's refinement calculus^{[912]} and PAR(Partition and Recur) method^{[13]} from the two core processes of program refinement and formal verification. In program refinement, the three methods all provide formal refinement rules, with Morgan's refinement calculus rules being the most numerous. However, only PAR method implements the complete program refinement process, from program specification to executable program(C++ program). In formal verification, the three methods all generate verification conditions manually and then perform manual verification. You et al^{[14]} enhanced the PAR method by replacing manual verification with mechanical verification via Isabelle. Table 1 compares the above mentioned automatic algorithm programming models in terms of program refinement and formal verification.
The current automatic programming model has two flaws. The first is the incompleteness of program refinement, and the second is the inadequate automation of formal verification. This paper presents an automatic algorithm programming model based on improved Morgan's refinement calculus to address these two issues. For the first deficiency, Morgan's refinement calculus is extended by adding quantifier specification transformation rules, and the C++ generation system is designed and implemented to complete the refinement process from specification to executable program. For the second deficiency, verification conditions are generated automatically based on VCG and mechanically verified by Isabelle. This is a significant step toward achieving high reliability and automation of the verification process.
Comparison of various automatic algorithm programming model
1 Automatic Algorithm Programming Model
The flow chart of automatic algorithm programming model proposed in this paper is shown in Fig. 1.
Fig. 1 Flow chart of automatic algorithm programming model 
1.1 Specification Generation
By analyzing user requirements, we generate an initial formal specification with pre and postconditions in specification generation. In this model, the specification is written as w:[P,Q]^{[10]}, where P is the precondition, Q is the postcondition, and w is the list of frame variables. The variables whose values may change, i.e. those in the list w above, are called the frame variables (or, more concisely, simply the frame) of the specification. The code that satisfies the specification w:[P,Q] may only change the value of one or more variables in w.
1.2 Specification Simplification
The generated specification could always be simplified to a lower complexity equivalent specification based on the analysis of concrete features of the specific field. We adopt the methods of problem division and specification transformation to simplify the specification.
1.3 Abstract Program Refinement Method
Definition 1(Sat) Sat(C,w:[P,Q]) is a predication that asserts the IMP(Imperative Programming Language) program C satisfies the specification w:[P,Q].
To make this idea more formal, the assertion that means X is refined by Y (or, equivalently, Y is a refinement of X) is denoted by X ⊆ Y, which is defined as follows^{[10]}.
Definition 2(Refinement) w:[P,Q] ⊆ w:[P',Q'] if and only if
∀C:IMP·Sat(C , w:[P',Q']) => Sat(C , w:[P,Q]).
Thus w:[P,Q] is refined by w:[P',Q'] if every IMP program that satisfies the specification w:[P',Q'] also satisfies the specification w:[P,Q].
The process of abstraction program refinement begins with the specification and ends with the abstract program (IMP program). Each step of the process adheres to the rules for demonstrating correctness. If these rules are applied strictly, we could end up with a correct IMP program^{[11]}.
In this model, the refinement of the abstract program is based on Morgan's refinement calculus. Morgan's refinement calculus provides refinement calculus rules for transforming one specification into another specification or an IMP statement. However, appropriate rules must be chosen by analyzing the specification. In one word, the specification should always be transformed in an equivalent manner to match the appropriate rules.
The Morgan's refinement calculus rules^{[6]} used in this model are shown in Table 2.
Quantifiers are used in specification to describe the preconditions and postconditions, but the refinement rules outlined above are insufficient to refine such specifications. In this model, we add some quantifier specification transformation rules, as shown in Table 3(Q_{a} is a quantifier, q_{a} is the binary operation corresponding to Q_{a}), which are used to transform the precondition or postcondition equivalently. The formalization of program refinement is optimized by expanding the available formal rules.
Morgan's refinement calculus rules
Quantifier specification transformation rules
1.4 Formal Verification
Artificial analysis during the refinement of an abstract program may result in program errors. Therefore, formal verification is required to ensure the correctness of the IMP program^{[12]}. Formal verification is divided into two steps. First, based on VCG, verification conditions are generated automatically by the IMP program. Second, the verification conditions are mechanically verified by Isabelle.
1.4.1 VCG
Hoare logic provability could be reduced to assertion language provability. In particular, if we want to prove a Hoare logical triple {P}c{Q}, we can compute an assertion A from it, and then {P}c{Q} is provable if A is provable. A is referred to as a verification condition, and the function that computes A is referred to as a verification condition generator, or VCG^{ [15]}.
The precondition and postcondition are provided as annotations to the VCG for all algorithm programs, and the invariant is additionally provided for WHILE loops. Figure 2 depicts the VCG code template for generating verification conditions.
Fig. 2 VCG code template for generating verification conditions 
The advantage of using VCG is that no human or machine is required to know the Hoare logic when trying to prove the generated validation conditions^{[15]}.
1.4.2 Isabelle theorem prover
Isabelle^{[1619]} is an auxiliary theorem prover who provides theorem proving with strong theoretical and technical support. Compared with other traditional theorem provers, the Isabelle theorem prover has the following distinguishing features. 1) Isabelle can handle multiple object logics. 2) Isabelle is in favor of new logic, which could be implemented by defining object logic's concrete syntax, abstract syntax, and inference rules. 3) Isabelle's verification language is Isar. It could accurately describe the system under test. Furthermore, Isar benefits from a wide range of data types, logic systems, and so on. 4) The editing tool jEdit could verify each step in the theorem proof, and display the proof status in the output panel.
1.5 IMP Program Refinement
We propose IMP program refinement to improve the completeness of program refinement. This refinement allows for the conversion of formally verified IMP programs to executable C++ programs. As a result, an automatic system known as the C++ generation system^{[2022]} is created, and the overall structure of the system is depicted in Fig. 3.
Fig. 3 The overall structure of the C++ generation system 
The system mainly consists of four modules: lexical analysis, syntactic analysis, semantic analysis and program transformation.
Lexical analysis transforms the IMP program character sequences into equivalent internal symbol sequences using IMP's lexical rules. Syntactic analysis identifies IMP syntactic items from internal symbol sequences using IMP syntax rules. Semantic analysis applies semantic processing to the syntactic items that have been identified. If the results of the above three analyses are incorrect, error messages will be reported in error handling. On the other hand, if the result is correct, the IMP program will be converted into a C++ program.
2 Example: A Stock's Maximum Income
2.1 Generating Problem Specification
2.1.1 Problem description
Suppose you could buy one share or sell your share per day at the stock's closing price. A stock's income is equal to the selling price minus the buying price. The problem with the maximum income of a stock is to calculate the maximum sum of the incomes from all possible trades over n days.
Figure 4 is an example of the volatility of a stock's closing price over n days.
Fig. 4 An example of the volatility of a stock's closing price 
2.1.2 Specification generation
The closing price of this stock in n days is stored in the array . According to the problem description, the essence of solving the problem is to find all the ascending segments P[i..j](P[i] and P[j] are the minimum value and the maximum value of the ascending segment respectively), then calculate the income P[j]P[i], finally add up the income of each ascending segment and the result of addition is maximum income.
Therefore, the maximum income of a stock in n days could be expressed by maxincome as:
The expression of the maxincome(n,P) is required when describing the specification of this problem. However, the specification would be complicated due to the complexity of this expression.
2.1.3 Specification simplification
In order to reduce the complexity of the specification, we could simplify the expression of the maxincome.
P[j]P[i] equals (P[i+1]P[i])+(P[i+2]P[i+1]) +…+ (P[j]P[j1]). For example, the incomefrom buying on day n2 and selling on day n5 is (P[n4]P[n5])+ (P[n3]P[n4])+(P[n2]P[n3]). Therefore, we could divide the array P[0..n1] into the n1 segments P[0,1], P[1,2], P[2,3],…, P[n2, n1], i.e. P[i1,i](1≤i≤n1). The maximum income could then be calculated by adding the incomes of all ascending segments ^{[23]}. It is obviously that whether P[i1,i] is an ascending segment or not is determined by the truth value of P[i1]<P[i].
Therefore, maxincome could be simplified to:
. We introduce a variable s to represent the maximum income calculated at some point in the process, then the postcondition of this problem could be expressed as: maxincome. Because the income of a stock is calculated from the second day, the precondition is n>1. In conclusion, the specification is as follows:
2.2 Refining Abstract Program
Figure 5 shows the whole process of refining abstract program, where①, ②, …, 14 represent program specifications and I_{1}, I_{2}, …, I_{6} represent refined IMP statements. The abstract program refinement ends when all of the specifications have been refined into IMP statements.
Fig. 5 Process diagram of abstract program refinement 
2.2.1 Choosing the invariantWe introduce a variable m(0<m≤n) to traverse the array P[0..n1] from left to right. When the subarray P[0..m1] is traversed, the maximum income maxincome(m,P) could be calculated, as shown in Fig. 6. Therefore the loop invariant could be defined as
inv≡s=maxincome(m,P)0<m≤n, which is similar to the postcondition(post≡s=maxincome(n,P)≡invm=n), so the program specification could be replaced equivalently by m,s:[n>1,invm=n]^{[16]}.
Fig. 6 Traversal process of calculating the maximum income 
2.2.2 Establishing the invariant
Before we can refine it to a loop, the general pattern for a specification should be something like w:[inv,inv¬G]. The following refinement process is required to get our refined specification into this shape^{[10]}.
According to Sequential Composition Rule, specification ② could be refined as:
Specification ③ : We could prove that 0<m+1≤nm_{0}<m+1≤n is true. Thus the specification ③ could be simplified to be viewed as some actions needed to establish the invariant(which must hold before the iteration could start)^{[10]}.
It should not be difficult to see that the assignment of m=1 and s=0 will be a suitable refinement.
We could prove that n>1=>inv[m,s\1,0] is true, thus the specifications ③ are refined as follows:
Thus, the result of "Establishing the Invariant" is:
2.2.3 Refining to create a loop
According to Repetition Rule, specification ④ could be refined to the following loop statement:
where V_{0} is the previous value of V.
V is defined as nm, and m_{0} is defined as the previous value of m, so we could get:
All that remains is to refine the body of the loop into code. Intuitively, we could see that m = m +1 is a good choice. Therefore specification ⑥ could be refined as follows:
After the above refinement, we have obtained the IMP statement (IMP statement I_{1}) that changes m, so we remove m from the frame variable. The specification is then updated as follows:
It is obvious that invm≠n=>invm≠nm_{0}=m is true, so:
Specifications ⑧ specifications ⑨, specifications ⑨ specifications ⑩:
We could prove that 0<m+1≤n<m+1≤n is true. Thus the specification ⑧ could be simplified to:
The next refinement is:
After observing the pre and postconditions of specifications ⑩, we analyze the relationship between maxincome(m,P) and maxincome(m+1,P):
Therefore, specification ⑩ would be refined as follows:
Specification 11 could be updated as follows by substituting maxincome(m,P) with its definition:
For refinement, there is no suitable Morgan's refinement calculus rule. However, using quantifier specification transformation rules, the postcondition could be transformed into a suitable shape:
It is easy to find:
The specification could then be transformed to:
We could prove that the following derivation is true.
Therefore the specification could be refined as follows:
In the same way, specification 12 could be refined as:
In conclusion, we could obtain the refinement of specification ⑩(IMP statement I_{7}) by integrating IMP statement I_{4}, I_{5}, I_{6}:
2.2.4 Putting IMP statements all together
We could now glue all of the pieces(IMP statement I_{1},I_{2},I_{3},I_{7}) together to get the code in Fig. 7 as a refinement of specification ①.
Fig. 7 IMP program of a stock's maximum income 
2.3 Formal Verification through Isabelle Based on VCG
The refinement process of Section 2.2 is accompanied by mathematical proof, ensuring manual reliability. However, it is not automatic and highly reliable. If the IMP program in Section 2.2.4 could be verified using Isabelle and VCG, the reliability of the automatic algorithm programming model could be ensured mechanically.
2.3.1 Automatically generating verification conditions based on VCG
Based on the IMP program obtained in Section 2.2.4, we insert the precondition and postcondition before and after the program respectively, and the loop invariant before the loop statement, as shown in top half of Fig. 8. The verification conditions could then be obtained(3 subgoals in bottom half of Fig. 8).
Fig. 8 Verification conditions generation based on VCG 
2.3.2 Mechanically verifying the generated conditions through Isabelle
The second subgoal in Fig. 8 generates two recursions, which can be transformed into two lemmas to assist us in verifying the second subgoal. The verification of the two lemmas is depicted in Fig. 9.
Fig. 9 Verification of the two recursions 
The next step is to verify the three subgoals in Fig. 8. After we call the Isabelle code "apply auto", there is only one subgoal to verify. This subgoal could be demonstrated automatically using the tool sledgehammer^{[24,25]}. Figure 10 depicts the outcome of applying sledgehammer for current verification. We can select the Isar proof code and click on it.
Fig. 10 Tool sledgehammer for auxiliary verification 
Figure 11 depicts the overall verification process for all the verification conditions.
Fig. 11 The overall verification process 
2.4 Refinement of the IMP Program
Through the C++ generation system, an IMP program could be refined to a C++ program. Figure 12 depicts the refinement process for the problem of a stock's maximum income, with the IMP program successfully verified on the left and the C++ program generated automatically on the right. Figure 13 depicts the testing of generated C++ program.
Fig. 12 Refinement from IMP program to C++ program 
Fig. 13 Testing of automatically generated C++ program 
3 Conclusion
This paper proposes an automatic algorithm programming model based on the improved Morgan's refinement calculus to improve the automation and reliability of algorithm programming. The model generates the program specifications according to user requirements. It refines step by step with formal verification and generates executable programs automatically with the help of the C++ generation system. An example of a stock's maximum income demonstrates the model's effectiveness. The model in this paper has the following characteristics in general.
1) Morgan's refinement calculus is extended by adding of quantifier specification transformation rules. Therefore, the formalization of program refinement is enhanced.
2) The manual generation of verification conditions for algorithm programs is replaced by the automatic generation. Therefore, formal verification automation is improved.
3) Based on the C++ generation system, abstract IMP programs are refined to executable programs. Therefore, the program refinement is more complete.
The automatic algorithm programming model allows for efficient programming while also ensuring the correctness of the generated program. However, two aspects of future work must be improved. One is to expand the refinement rule library to further optimize Morgan's refinement calculus, and the other is to apply the model to more complex data structures.
References
 Chinese Academy of Sciences. Chinese Discipline Development Strategy: Software Science and Engineering [M]. Beijing: Science Press, 2020(Ch). [Google Scholar]
 Wang J, Zhan N J, Feng X Y, et al. Overview of formal methods [J]. Journal of Software, 2019, 30(1): 3361(Ch). [Google Scholar]
 Michael J B, Dinolt G W, Drusinsky D. Open questions in formal methods [J]. Computer, 2020, 53(5): 8184. [CrossRef] [Google Scholar]
 Schaffer K, Voas J. What happened to formal methods for security? [J]. Computer, 2016, 49(8): 7079. [CrossRef] [Google Scholar]
 Brooks F P, Frederick P. The Mythical ManMonth [M]. Beijing: People Post Press, 2010(Ch). [Google Scholar]
 Dijkstra E W. A Discipline of Programming [M]. Englewood: Prentice Hall, 1976. [Google Scholar]
 Dijkstra E W, Feijen W. A Method of Programming [M]. London: AddisonWesley Publishing Company, 1988. [Google Scholar]
 Gu T L. Formal Method of Software Development [M]. Beijing: Higher Education Press, 2005(Ch). [Google Scholar]
 Morgan C. Programming from Specifications [M]. Englewood: Prentice Hall, 1998. [Google Scholar]
 Kourie D G, Watson B W. The CorrectnessbyConstruction Approach to Programming [M]. Berlin: SpringerVerlag, 2012. [CrossRef] [Google Scholar]
 Watson B W, Kourie D G, Cleophas L. Experience with correctnessbyconstruction [J]. Science of Computer Programming, 2015, 97(1):5558. [CrossRef] [Google Scholar]
 Runge T, Schaefer I, Cleophas L, et al. Tool support for correctnessbyconstruction [C]// International Conference on Fundamental Approaches to Software Engineering. Cham: SpringerVerlag, 2019: 2542. [Google Scholar]
 Xue J Y, You Z, Hu Q M, et al. PAR: A practicable formal method and its supporting platform [C]// International Conference on Formal Engineering Methods. Cham: SpringerVerlag, 2018: 7086. [Google Scholar]
 You Z, Xue J Y, Zuo Z K. Unified formal derivation and automatic verification of three binarytree traversal nonrecursive algorithms [J]. Cluster Computing, 2016, 19(4): 21452156. [CrossRef] [Google Scholar]
 Nipkow T, Klein G. Concrete Semantics with Isabelle/HOL [M]. Berlin: SpringerVerlag, 2020. [Google Scholar]
 Li Y, Pang J. Formalizing provable anonymity in Isabelle/HOL [J]. Formal Aspects of Computing, 2015, 27(2):255282. [CrossRef] [MathSciNet] [Google Scholar]
 Stannett M, Nemeti I. Using Isabelle/HOL to verify firstorder relativity theory [J]. Journal of Automated Reasoning, 2014, 52(4): 361378. [CrossRef] [MathSciNet] [Google Scholar]
 Paulson L C. A mechanised proof of gdel's incompleteness theorems using nominal Isabelle [J]. Journal of Automated Reasoning, 2015, 55(1): 137. [CrossRef] [MathSciNet] [Google Scholar]
 Yushkovskiy A, Tripakis S. Comparison of two theorem provers: Isabelle/HOL and Coq [C]// Proceedings in Computer Science. Helsinki: Aalto University, 2018:118. [Google Scholar]
 Lai Y. Development of APLA to C++ Automatic Program Conversion System [D]. Nanchang: Jiangxi Normal University, 2002(Ch). [Google Scholar]
 Zuo Z K, Liu Z H, Huang Q, et al. The comparative study on the generic features of Apla and programming languages [J]. Journal of Jiangxi Normal University (Natural Sciences Edition), 2019, 43(5): 454461(Ch). [Google Scholar]
 Zhang Q, Wang C J, Luo H M, et al. The generation method and automatical transformation system of WSDL→RadlWS [J]. Journal of Jiangxi Normal University (Natural Sciences Edition), 2018, 42(3): 298303(Ch). [Google Scholar]
 Qi L L, Yang Q H, You Y. Formal derivation of algorithm and automatic verification based on Isabelle [J]. Journal of Jiangxi Normal University (Natural Sciences Edition), 2018, 42(4):379383(Ch). [Google Scholar]
 Si X, Dai H, Raghothaman M, et al. Learning loop invariants for program verification [C]∥Proceedings of the 32nd International Conference on Neural Information Processing Systems. Montreal: Neural Information Processing Systems Foundation, 2018: 77627773. [Google Scholar]
 Nipkov T, Paulson T. HighOrder Logic Auxiliary Proof System [M]. Beijing: Beijing Institute of Technology Press, 2013. [Google Scholar]
All Tables
All Figures
Fig. 1 Flow chart of automatic algorithm programming model  
In the text 
Fig. 2 VCG code template for generating verification conditions  
In the text 
Fig. 3 The overall structure of the C++ generation system  
In the text 
Fig. 4 An example of the volatility of a stock's closing price  
In the text 
Fig. 5 Process diagram of abstract program refinement  
In the text 
Fig. 6 Traversal process of calculating the maximum income  
In the text 
Fig. 7 IMP program of a stock's maximum income  
In the text 
Fig. 8 Verification conditions generation based on VCG  
In the text 
Fig. 9 Verification of the two recursions  
In the text 
Fig. 10 Tool sledgehammer for auxiliary verification  
In the text 
Fig. 11 The overall verification process  
In the text 
Fig. 12 Refinement from IMP program to C++ program  
In the text 
Fig. 13 Testing of automatically generated C++ program  
In the text 
Current usage metrics show cumulative count of Article Views (fulltext 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 4896 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.