Issue 
Wuhan Univ. J. Nat. Sci.
Volume 28, Number 3, June 2023



Page(s)  246  256  
DOI  https://doi.org/10.1051/wujns/2023283246  
Published online  13 July 2023 
Computer Science
CLC number: TP311
Nonlinear Program Construction and Verification Method Based on Partition Recursion and Morgan's Refinement Rules
^{1}
College of Computer Information Engineering, Jiangxi Normal University, Nanchang 330022, Jiangxi, China
^{2}
College of Digital Industry Academy, Jiangxi Normal University, Shangrao 334000, Jiangxi, China
^{†} To whom correspondence should be addressed. Email: zhengkang2005@iscas.ac.cn
Received:
21
May
2022
The traditional program refinement strategy cannot be refined to an executable program, and there are issues such as low verification reliability and automation. To solve the above problems, this paper proposes a nonlinear program construction and verification method based on partition recursion and Morgan's refinement rules. First, we use recursive definition technique to characterize the initial specification. The specification is then transformed into GCL(Guarded Command Language) programs using loop invariant derivation and Morgan's refinement rules. Furthermore, VCG (Verification Condition Generator) is used in the GCL program to generate the verification condition automatically. The Isabelle theorem prover then validates the GCL program's correctness. Finally, the GCL code generates a C++ executable program automatically via the conversion system. The effectiveness of this method is demonstrated using binary tree preorder traversal program construction and verification as an example. This method addresses the problem that the construction process's loop invariant is difficult to obtain and the refinement process is insufficiently detailed. At the same time, the method improves verification process automation and reduces the manual verification workload.
Key words: program construction / partition recursion / Morgan's refinement rules / loop invariant / VCG / Isabelle theorem prover
Biography: WANG Changjing, male, Ph.D., Professor, research direction: software formal method, trustworthy software. Email: wcj771006@163.com
Fundation item: Supported by the National Natural Science Foundation of China (62262031), Science and Technology Key Project of Education Department of Jiangxi Province (GJJ2200302, GJJ210307), and the Graduate Innovative Special Fund Projects of Jiangxi Province (YJS2022064)
© Wuhan University 2023
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
With the continuous progress of computer technology and the expansion of application areas, software security has received wide attention from the society. The use of formal methods^{[14]} to develop programs can strictly guarantee the correctness and reliability of programs. Formal methods also help to better understand the functions and behaviors of programs and meet user requirements. Therefore, formal methods have a wide range of promising applications in software development. Program derivation and verification techniques are the hot spots in the research of formal methods. The more mature techniques are Dijkstra's weakest predicate method^{[5,6]}, Morganbased program derivation methods^{[79]}, and PAR(PartitionandRecur) methods^{[4]}.
Dijkstra's weakest predicate approach defines its own language rules by which programs can be developed and verified. The advantage is that the development process is strictly based on mathematical logic and formal verification is performed during the development process. However, the verification process is mostly manual and less automated; and the abstract programs obtained by this method cannot be converted into executable programs.
The PAR method transforms the initial specification by its own defined rules to obtain recursive equations and loop invariant, which eventually lead to an abstract Apla program^{[4]}. The advantage of this method is that the derivation process is guided by a system with its own derivation patterns and rules, which are more widely applicable. However, the procedure of program derivation using this method is not sufficiently refined and the obtained Apla abstract program is not mechanically proven and has a low automation procedure.
This paper proposes a program construction and verification method based on partition recursion and Morgan's refinement rule. The method first transforms the initial program specification by recursive definition technique, and then obtains recurrence relations and loop invariant by using partitioned recursion rules^{[10,11]}. Then, based on the loop invariant, the program specification is gradually refined using Morgan refinement rules to finally obtain a reliable abstract program. The verification conditions are obtained by VCG^{[12]}(Verification Condition Generator) and then verified by Isabelle^{[1214]} theorem provers. After the verification, the obtained abstract program is then generated into a C++ program through the conversion system^{[15]} to realize the whole process from abstract specification to abstract program^{[15,16]}, then mechanical verification^{[16,17]}, and to executable program.
The paper is organized as follows. Section 1 focuses on detailing the program construction and verification methods based on partition recursion and Morgan's refinement rule; Section 2 takes the binary tree preorder problem^{[18,19]} as an example to develop and verify the binary tree problem using the methods proposed in this paper as a guide; Section 3 concludes the whole paper.
1 Proposed Method of Nonlinear Program Construction and Verification
This section focuses on the method proposed in this paper. The method in this paper contains a complete set of program construction and verification methods, which mainly consists of four steps, as shown in Fig.1.
Fig. 1 Proposed method of nonlinear program construction and verification 
1.1 Initial Specification Generation
A program specification is a detailed description of a program's functions. It expresses a precise description of the problem in an easytounderstand manner for the implementer. The program specification consists primarily of the program's preassertion P and postassertion Q. P and Q are conditions that must be met before and after program input, respectively.
Hoare's formal specification is primarily in the form of triples {P}S{Q}^{[13]}, but this paper primarily uses Morgan's specification representation w:[P, Q]. Morgan rewrote the Hoare triples representation to make the specification representation more compact and easier to refine into code.
1.2 Program Refinement and Generation
1.2.1 Initial specification transformation
Following the generation of the initial specification, the attributes of firstorder logic are typically used to gradually refine the specification transformation from the postpredicate. After the generation of the binary tree preorder specification in Section 1.1, the initial specification transformation needs to be performed on it. The following is the specific transformation procedure.
Due to the binary tree's easy decomposition, this paper first introduces the recursive function of the binary tree and strengthens the postprediction of initial specification. Then, Morgan's framework variables are introduced to convert the initial reduction's triple form into a Morganspecific symbolic form. Figure 2 depicts the entire initial specification transformation process. This recursive technique reduces the difficulty of changing the binary tree specification. At the same time, recursion technology provides a foundation for subsequent programs to use partition recursion to find loop invariant.
Fig. 2 Initial specification conversion process 
1.2.2 Loop invariant derivation
Acquiring loop invariant has always been a difficult point in formal derivation, and acquiring tree structure loop invariant is even more difficult. To address this issue, this paper proposes the use of partition recursion in conjunction with recursive definition technology to derive the loop invariant of tree structure.
The basic idea behind partition recursion is to divide a large, difficulttosolve problem into some smaller problems of the same scale, and then find the recurrence relationship via the relationship between subproblems.
First, this paper decomposes the original problem using the recursive definition technique. The recurrence relationship between the problems is then determined based on the relationship between the subproblems in the decomposition process. Finally, the binary tree's loop invariant is discovered using the recursive relationship. Figure 3 depicts the specific process flow.
Fig. 3 Loop invariant derivation process 
1.2.3 Morgan’s rules refinement
The initial statute and loop invariant have been obtained in Sections 1.2.1 and 1.2.2. Now it is necessary to derive the initial specification to the GCL program based on loop invariant, which are used as Morgan's refinement rules in this paper. Morgan's refinement rules are used to gradually refine the abstract specification into GCL^{[8,9] }code with strong execution, with each refinement step being small and easy to handle. Using the Morgan's refinement rules, each step of the refinement process must be guaranteed to be justified and proven. As a result, the program obtained is extremely reliable.
The rules used in the Morgan refinement method are specified in Table 1^{[8]} .
Morgan's refinement rules
1.3 GCL Program Automation Verification
The GCL program obtained in Section 1.2 needs to be mechanically verified by generating verification conditions through VCG and by Isabelle. The specific steps are shown as follows.
1.3.1 Verification condition generation
The automatic generation of verification conditions is mainly done through VCG, which aims at converting the verification of Hoare triples into the verification of assertions. The advantage of this is that the person or machine verifying the program does not need to know anything about Hoare logic to be able to prove the program.
VCG is a verification condition generator whose working process relies on two conversion functions: pre (this function is different from the following binary tree preorder function Prebt) and vc function. pre function mainly converts the imperative program into specific Hoare logic rules, and vc function mainly converts the result of pre function into specific verification conditions. The specific VCG working schematic is shown in Fig.4 .
Fig. 4 Working principle of VCG 
1.3.2 Isabelle assisted verification
Manual and mechanical verification are the two types of formal verification technology. Manual verification is more difficult and prone to errors. Mechanical verification is based on mathematical logic, and it is far more efficient and reliable than manual verification. The mechanical theorem prover^{[16]} is further subdivided into automatic and interactive theorem provers.
Isabelle, an automatic theorem prover, is chosen for auxiliary verification in this paper, primarily because Isabelle has the following advantages.
1) The powerful rule base
Isabelle has a powerful rule base, in which every theory contains many related rules and theorems. More importantly, users can add theorems and prove them based on their own proof requirements. If the newly added theorem passes the proof, the Isabelle system will save the newly added lemma and use it in the theorem's subsequent proof.
2) The Sledgehammer tool
The Isabelle system's Sledgehammer^{[12,13]} tool is extremely powerful, and it can invoke several other automatic theorem provers to find theorems, including E, SPASS, Vampire, and others. In the Isabelle operator interface, the user only needs to click on the apply application in the Sldgehammer button and Slagehammer can automatically generate the proof process. The user then clicks on the proof process to automatically insert theproof process into the Isabelle script.
1.4 Conversion from GCL Program to Executable Program C++
The GCL programs verified in Section 1.3 are still abstract and cannot be compiled and executed on a computer. As a result, the GCL program will need to be converted into an executable file. First, we can convert the GCL program to an Apla program. GCL and Apla can be converted because they are abstract imperative programs with similar syntax. Then, using the team's Apla to C++ program automatic converter, convert the above Apla abstract program into an imperative C++ program. The team's Apla to C++ conversion system is depicted in Fig.5.
Fig.5 Apla to C++ conversion system 
With these four steps, this paper realizes the whole process of program development, verification and transformation.
2 Example: Binary Tree Preorder Problem (BTPP)
2.1 Initial Specification Generation of BTPP
Preorder traversal is a way of traversing a binary tree. By preorder traversal, we mean that when traversing a binary tree, we first traverse the root node, then the left subtree, and finally the right subtree. In this paper, we use T to represent a binary tree, and thePrebt (T) function to represent the preorder traversal of the entire binary tree T. Therefore, the binary tree preorder traversal specification can be expressed as follows:
2.2 Program Refinement of BTPP
2.2.1 Initial specification transformation
There are two types of binary tree traversal algorithms: recursive traversal and nonrecursive traversal. The goal of this paper is to deduce the binary tree's preorder nonrecursive algorithm program.
This section focuses on the initial specification transformation, which is the transformation of the posterior assertion Prebt. And we know that the process of binary tree preorder traversal is to traverse the root node, then the left subtree, and then the right subtree. So the Prebt function can be written first as follows:
We decompose this function according to the content of the Prebt function, and we can obtain the following derivation process:
Figure 6 depicts the binary tree's change process as a result of the recursive function Prebt. As shown in the derivation and Fig.6, the root node is retained first when traversing a binary tree recursively. The left subtree of the tree will then be traversed, followed by the right subtree of the tree. As a result, three variables, X, q, and S, are introduced. The nodes that have been traversed are stored in the sequence X. The sequence S is used to store the nodes to be traversed, while q is used to store the subtree of T that is about to be traversed. The original specification can then be refined as needed:
Fig. 6 The process of binary tree change under the action of recursive function 
2.2.2 Loop invariant derivation
We have obtained the initial specification after the transformation, next we need to obtain the corresponding loop invariant. In this paper, the loop invariant are obtained according to the division recursion, i.e., we find the law and obtain the loop invariant in the process of binary tree traversal in the preorder.
As illustrated in Fig.7, for the traversed subtree q, the subtree's head node is always stored in X, and q continues to traverse the subtree's left subtree. The right subtree of the subtree is still in S.
Fig. 7 Binary tree traversal node change process diagram 
After traversing subtree q, the next round will continue to find nodes from sequence S to traverse. The sequence 's length will be reduced accordingly. The definition of the recurrence relation F function can be derived:
We can see from the previous Prebt and F functions that the binary tree preorder traversal process always places the nodes traversed by q in the sequence X. Then q continues to traverse the subtree's remaining nodes to the left. After traversing the left subtree, q will look for nodes in the sequence S to continue traversing, as shown in Fig.8. So the loop invariant is .
Fig. 8 Loop invariant derivation process diagram 
2.2.3 Morgan's rules refinement
1) Loop variable initialization
Based on loop invariant obtained in Section 2.2.2, the specification can be refined using Strengthen postcondition in Table 1, and the specification can then be obtained as:
According to the specification, inv is used as an intermediate assertion connecting the prepredicate and the postpredicate, then (5) is refined using Sequential composition in Table 1:
Assignment in Table 1 is used to refine (6), and the following formula is obtained:
Because:
So the first part of the refinement is established.
2) Loop process refinement
Formula (7) can be refined using Repetition in Table 1, and ¬(X = Pre(T)) is a loop condition and can be equivalently converted to , then the following equation can be obtained:
The variable in the above equation is the marker for the terminability proof. needs to satisfy two conditions: first, it must be guaranteed to be decremented in each loop, and second, it cannot be decremented to a negative number. In this paper, we need to find the specific terminability variable .
We can see here that the variable X stores the nodes that are traversed. And the number of nodes in X keeps increasing. When the loop is completed, the number of nodes stored in X is equal to the number of nodes in the binary tree T. So, we can select (T#X) (T is the node value of the whole binary tree and X is the stored traversed node value) as the variable .
We can simplify the equation by substituting v=T#X for:
Then (9) is simplified to:
Under the premise of , the above formula can be further refined according to Selection in Table 1.
The above equation (10) can be further refined according to Assignment in Table 1:
because
According to the definition of inv, Prebt, and F functions, the above formula can be simplified:
Left side:
Right side:
So
Similarly, the above equation (11) can be further refined according to Assignment in Table 1.
According to the above refinement, the program can be replaced by:
if
Combined with the above formula, the final GCL program is:
do
if
2.3 GCL Program Automation Verification of BTPP
2.3.1 Verification condition generation
In order to verify the GCL code obtained in Section 2.2.3 above, we must first construct the lemma Pre_bt. Then, using the GCL code from above, we must write the corresponding code in Isabelle. The two have the same code structure, and the Isabelle code is as follows:
lemma Pre_bt: "VARS X S T q
{true}
X :=[];q:=T;S :=[];
WHILE(q≠Tnull q=TnullS≠[])
INV{Prebt(T)=X@Prebt(q)@F(S)}
DO
IF q≠TnullTHEN
X :=X@[data q];
S :=[rtree q]@S ;
q :=(ltree q)
ELSE IF q=TnullS≠[]THEN
q :=(hd S);
S :=(tl S)
ELSE
SKIP
FI
OD
{X=Prebt(T)}"
We then use the apply vcg command to get three verification conditions, as shown in Fig.9.
Fig. 9 Verification condition generation 
2.3.2 Isabelle assisted verification
Some auxiliary functions and lemmas are required to verify the above three subgoals. The following are the specific steps:
1) Define two recursive functions Prebt, F:
Function 1:
primrec Prebt::"'a BTree⇒'a list"
where
"Prebt Tnull=[]""Prebt(BT t1 x t2) =[x]@(Prebt t1)@(Prebt t2)"
Function2:
fun F::"'a BTreelist⇒'a list"
where
"F[] =[]""F(x#xs) =(Prebt x)@(F xs)"
2) Create the lemmas prebt_rule and F_rule to prove the final program.
Lemma 1:
lemma prebt_rule[simp]:"q≠TnullPrebt q =data q#Prebt(ltree q)@Prebt(rtree q)"
apply(induct q)
apply auto
done
Lemma 2:
lemma F_rule[simp]:"xs≠[]F xs=Prebt(hd xs)@F(tl xs)"
apply(induct xs)
apply auto
done
3) Prove the three subgoals:
apply auto
With the auto command in 3) above, we can get a successful result of verification. This is shown in Fig.10.
Fig.10 Verification success result diagram 
2.4 Conversion from GCL Program to Executable Program C++ of BTPP
For the verified GCL program in Section 2.2.3, it is a nonexecutable abstract program that needs to be converted to executable C++. First, the GCL program needs to be equivalently converted to an Apla program because their syntax is similar. The resulting Apla program is then passed through our team's conversion system to generate a C++ program, and the conversion result is shown in Fig.11. Finally, the converted C++ program is compiled and run, and the running result is shown in Fig.12.
Fig. 11 Apla to C++ program 
Fig. 12 Operation result graph 
3 Conclusion
This paper proposes a new method for building and verifying nonlinear programs. Using the preorder traversal of a binary tree as an example, an abstract program GCL is created from the initial specification. Isabelle validates GCL programs before converting them to executables using the C++ conversion platform. The following are the primary benefits of this paper:
1) Partition recursion is used throughout the program construction process to derive loop invariant. The specification is then gradually refined by Morgan's refinement rule based on loop invariant. This method ensures the acquisition of loop invariant while also refining the program.
2) The method first employs VCG to generate verification conditions automatically. The verification conditions are then mechanistically verified using Isabelle. This greatly improves verification automation.
3) This method improves the method's integrity by converting the obtained abstract program GCL into a C++ executable program using the C++ conversion platform.
Our next step is to use this approach and combine it with our previous work^{[2025]} to derive and synthesize more complex algorithms for nonlinear data structures, such as those related to binary trees or graphs.
References
 Gu T L. The Formal Method of Software Development[M]. Beijing: Higher Education Press, 2005(Ch). [Google Scholar]
 Wang J, Zhan N J, Feng X Y , et al. An 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]. IEEE Annals of the History of Computing, 2020, 53(5): 8184. [CrossRef] [Google Scholar]
 Xue J, Zheng Y, Hu Q, et al. PAR: A practicable formal method and its supporting platform[C]// International Conference on Formal Engineering Methods. Cham: SpringerVerlag, 2018: 7086. [Google Scholar]
 Dijkstra E W. A Discipline of Programming [M]. Englewood Cliffs: Prentice Hall, 1976. [Google Scholar]
 Dijkstra E W , Feijen W. A Method of Programming[M]. Boston: AddisonWesley Longman Publishing Co. Inc., 1988. [Google Scholar]
 Morgan C. Programming from Specifications[M]. Upper Saddle River : PrenticeHall, Inc., 1990. [Google Scholar]
 Kourie D G, Watson B W. The CorrectnessbyConstruction Approach to Programming[M]. Berlin: Springer Science & Business Media, 2012. [CrossRef] [Google Scholar]
 Runge T , Schaefer I , Cleophas L , et al. Tool support for correctnessbyconstruction[C]//International Conference on Fundamental Approaches to Software Engineering. Berlin: SpringerVerlag, 2019: 2542. [Google Scholar]
 Si X, Dai H J, Raghothaman M, et al. Learning loop invariant for program verification[C]//Proceedings of the 32nd International Conference on Neural Information Processing Systems. Montreal: Neural Information Processing Systems Foundation, 2018. [Google Scholar]
 Gries D. A note on a standard strategy for developing loop invariant and loops[J]. Science of Computer Programming, 1982, 2(3): 207214. [CrossRef] [MathSciNet] [Google Scholar]
 Nipkow T, Klein G. Concrete Semantics with Isabelle/HOL[M]. Berlin: Springer International Publishing, 2014. [CrossRef] [Google Scholar]
 Nipkow T, Markus W, Lawrence C. Isabelle/HOL: A Proof Assistant for HigherOrder Logic[M]. Berlin, Heidelberg: SpringerVerlag, 2002. [Google Scholar]
 Benzmüller C , Claus M , Sultana N. Systematic verification of the modal logic cube in Isabelle / HOL[J] . Electronic Proceedings in Theoretical Computer Science, 2015, 186: 2741. [CrossRef] [MathSciNet] [Google Scholar]
 Lai Y. Development of APLA to C++ Automatic Program Conversion System [D]. Nanchang : Jiangxi Normal University, 2002(Ch). [Google Scholar]
 Jiang N, Li Q A, Wang L M, et al. Review of mechanized theorem proof research [J]. Journal of Software, 2020, 31(1): 82112(Ch). [Google Scholar]
 Tobias N K, Lawrence P S. Auxiliary Proof System for Higher Order Logic[M]. Beijing: Institute of Technology Press, 2013(Ch). [Google Scholar]
 Zuo Z K, Fang Y, Huang Q, et al. Derivation and formal proof of binary tree sorting nonrecursive Algorithm[J]. Journal of Jiangxi Normal University(Natural Science Edition), 2020, 44(6): 625632(Ch) . [Google Scholar]
 You Z, Xue J Y. Formal verification of algorithm program based on Isabelle theorem prover[J]. Computer Engineering and Science, 2009, 31(10): 8589(Ch). [NASA ADS] [Google Scholar]
 Zhang Q F, Wang C J, Zuo Z K, et al. The formal verification method for smart contract properties based on UPPAAL[J]. Journal of Jiangxi Normal University: Natural Science Edition, 2023, 47(1): 4551(Ch). [Google Scholar]
 Wang C J, Chen X, Ding X L, et al. The Web service symbolic execution and verification based on modeldriven[J]. Journal of Jiangxi Normal University: Natural Science Edition, 2022, 46(1): 3748(Ch). [Google Scholar]
 Zuo Z K, Fang Y, Huang Z P, et al. The derivation and formal proof of nonrecursive algorithm for binary tree queue relation problems[J]. Journal of Jiangxi Normal University: Natural Science Edition, 2022, 46(1): 4958(Ch). [Google Scholar]
 Yu X J, Wang C J, Qu W J, et al. The prediction of epidemic trend of COVID19[J]. Journal of Jiangxi Normal University: Natural Science Edition, 2021, 45(6): 559565(Ch). [Google Scholar]
 Wang C J, He J F, Luo H M, et al. The modeldriven Dafny program generation and automatic verification[J]. Journal of Jiangxi Normal University: Natural Science Edition, 2020, 44(4): 378384(Ch). [Google Scholar]
 Wang C J, Yu X J, Shen D M, et al. The twolevel verification method of shared memory concurrent distributed algorithm based on concurrent Apla language[J]. Journal of Jiangxi Normal University: Natural Science Edition, 2020, 44(3): 301306(Ch). [Google Scholar]
All Tables
All Figures
Fig. 1 Proposed method of nonlinear program construction and verification 

In the text 
Fig. 2 Initial specification conversion process 

In the text 
Fig. 3 Loop invariant derivation process 

In the text 
Fig. 4 Working principle of VCG 

In the text 
Fig.5 Apla to C++ conversion system 

In the text 
Fig. 6 The process of binary tree change under the action of recursive function 

In the text 
Fig. 7 Binary tree traversal node change process diagram 

In the text 
Fig. 8 Loop invariant derivation process diagram 

In the text 
Fig. 9 Verification condition generation 

In the text 
Fig.10 Verification success result diagram 

In the text 
Fig. 11 Apla to C++ program 

In the text 
Fig. 12 Operation result graph 

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.