Issue 
Wuhan Univ. J. Nat. Sci.
Volume 26, Number 6, December 2021



Page(s)  481  488  
DOI  https://doi.org/10.1051/wujns/2021266481  
Published online  17 December 2021 
Computer Science
CLC number: TP305
A Method to Deduce and Synthesize the Dafny Programs
^{1}
College of Computer Information Engineering, Jiangxi Normal University, Nanchang
330022, Jiangxi, China
^{2}
Management Science and Engineering Research Center, Jiangxi Normal University, Nanchang
330022, Jiangxi, China
^{3}
College of Physics and Communication Electronics, Jiangxi Normal University, Nanchang
330022, Jiangxi, China
† To whom correspondence should be addressed. Email: zhengkang2005@iscas.ac.cn
Received:
16
October
2021
We propose a systematic method to deduce and synthesize the Dafny programs. First, the specification of problem is described in strict mathematical language. Then, the derivation process uses program specification transformation technology to perform equivalent transformation. Furthermore, Dafny program is synthesized through the obtained recursive relationship and loop invariants. Finally, the functional correctness of Dafny program is automatically verified by Dafny verifier or online tool. Through this method, we deduce and synthesize Dafny programs for many typical problems such as the cube sum problem, the minimum (or maximum) contiguous subarray problems, several searching problems, several sorting problems, and so on. Due to space limitation, we only illustrate the development process of Dafny programs for two typical problems: the minimum contiguous subarray problem and the new local bubble sorting problem. It proves that our method can effectively improve the correctness and reliability of Dafny program developed. What’s more, we demonstrate the potential of the deductive synthesis method by developing a new local bubble Sorting program.
Key words: Dafny / deductive synthesis / specification transformation technology / recursive relationships / loop invariants
Biography: WANG Changjing, male, Ph. D., Professor, research direction: software formal method, trustworthy software. Email: wcj771006@163.com
Foundation item: Supported by the National Natural Science Foundation of China (61762049, 61862033, 61902162 ,11804133) and Natural Science Foundation of Jiangxi Province (20202BABL202025, 20202BABL202026, 20202BAB202015)
© Wuhan University 2021
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
From the perspective of computer science, it is almost impossible to create completely reliable software except for very small programs^{[1]}. We have known for decades about the principles and techniques for ensuring that programs are correct, but it is not easy to verify the program correctly. As verification tools become powerful and practical in the past decade, it makes formal software verification feasible. For example, in order to improve the efficiency and reliability of software development, Microsoft recruits experts and outstanding graduates to specialize in the research of formal methods and verification tools. At the same time, with the rapid development of automatic proof theory, the improvement of CPU computing power, and the enhancement of theorem prover, the program proof tasks emerge in large numbers, and many welldesigned program provers appear^{[2]}.
With the development of formal verification technology, the successful application of formal verification tools in program verification continues to increase. Due to the advantages of formal methods^{[3]} in the development of complex and reliable software, formal verification tools will significantly improve our efficiency in verifying reliable algorithm software in the future. In addition, formal verification tools have the following advantages: higher verification efficiency and no need to write certificates manually. Dafny, one of the most representative formal verification tools, can verify the correctness of the program and provide complete automation, and also can reduce the workload of our comprehensive verification of the program^{[4]}.
This paper uses formal method to develop Dafny programs for two typical problems: the minimum contiguous subarray problem and the new local bubble sorting problem. The final developed programs are automatically verified by Dafny verifier. The main contributions are as follows:
1) We propose a system method to deduce and synthesize the Dafny programs. Initially, the specification of problem is described in strict mathematical language. Then, the derivation process uses program specification transformation technology to perform equivalent transformation. Furthermore, Dafny program is synthesized through the obtained recursive relationship and loop invariants. Finally, the functional correctness of Dafny program is automatically verified by Dafny verifier or online tool.
2) We deduce and synthesize Dafny programs for many typical problems such as the cube sum problem, the minimum (or maximum) contiguous subarray problems, several searching problems, several sorting problems. Due to space limitation, we only illustrate the development process of Dafny by focusing on two typical problems: the minimum contiguous subarray problem and the new local bubble sorting problem. It proves that our method can effectively improve the correctness and reliability of the developed Dafny program.
3) We demonstrate the potential of the deductive synthesis method by developing a new Local Bubble Sorting program.
The organizational structure of this article is as follows: Section 1 is the introduction of related work; Section 2 is about related technologies and tool, briefly introducing the specification transformation technology and Dafny; Section 3 is the deductive synthesis Dafny programs for minimum contiguous subarray problem and bubble sorting problem; Section 4 is conclusion and future work.
1 Related Work
In this section, we survey prior work that are closely related to the method proposed in this paper.
Program synthesis. There has been a great deal of interest in automated synthesizing programs from highlevel expressions of user intent^{[57]} in the past decade. Some of these techniques are geared towards computer endusers and they utilize informal specifications such as inputoutput examples, natural language, or a combination of both. On the other hand, program synthesis techniques are geared towards programmers who often utilize additional information, such as a program sketch or types in addition to test cases or logical specifications. Most of the program synthesis methods are obtained from semiformal description (such as UML) or unformal description (such as natural language). The main difference between those methods and ours is that we deduce the Dafny program from formal specification, which is helpful to subsequent formal reasoning. In addition, our method synthesizes recursive relationships and loop invariants to develop the Dafny programs.
Program transformation. Program transformation was introduced by researchers 50 years ago, and then it was formalized^{[810]}. From then on, program transformation technology has gradually developed. Program transformation converts one program into another^{[10]}. Learnig the idea of program transformation, we design the specification transformation technology. Program transformation converts an initially inefficient program into an equivalent program. Our method is different from program transformation by generating an effective algorithm from the problem specification. We also learn from the idea of transformation strategies^{[1113]} to get better transform rules.
Program refinement ^{[14]}. At present, some good program refinement work has been applied to practice. The authors of Refs.[1517] proposed a mechanism to gradually refine the specification into executable code by introducing implementation details. In our method, we use strict formal derivation technology and specification transformation technology to make the final derivation procedure more rigorous and correct.
2 Related Technology and Tool
In this section, we mainly introduce program specification transformation technology and Dafny.
2.1 Program Specification Transformation Technology
The proof of correctness of program, formal derivation and functions depends on whether the specification is correct and whether the construction is proper either to a great extent. Some quantifiers should be used when describing the program specification of the problem^{[18]}. The general form is: (Qi:r(i):f(i)), r(i) is the range of the constraint variable i, and f(i) is the function of the constraint variable. The meaning of this form is “the quantity obtained by performing q operation on the function f(i) in the range of r(i)”. The quantifier Q mainly includes ∀(universal quantifier), ∃(existential quantifier),∑(summation quantifier),∏(quadrature quantifier), MIN(minimum quantifier), MAX(maximum quantifier), N(count quantifier), etc^{[19]}. What we mentioned below will be used in the transformation of program specification.
1) Range division
(Qi :r(i): f(i))=(Qi : r(i)∧b(i) :f(i))q(Qi :r(i)∧¬b(i): f(i))
2) Crossproduct nature
(Qi, j :r(i)∧s(i, j): f(i, j))=(Qi :r(i):(Qj :s(i, j) :f(i, j)))
3) Single range
(Qi: i = k:f(i)) = f(k)
4) General distribution law
(Qi: r(i):g(i) q f(i))= (Qi :r(i): g(i))q(Qi :r(i): f(i))
where i is not a free variable in g.
2.2 Dafny Overview
Dafny is a programming language and static program prover. The Dafny language combines functional programming and objectbased programming paradigms. It supports generic classes and dynamic allocation, with builtin specification structures (like Eiffel, JML, and Spec#)^{[20]}. Dafny programming language supports static verification of the program, and it contains annotations for specifying programs. Annotations include preconditions and postconditions, framing specifications (reads and modifies sets), loop invariants, and termination metrics. To further support the specification, the language also provides updatable ghost variables, userdefined functions, algebraic data types, sets, and sequences. These features allow modular verification^{[21]} of the specified program, so the individual verification of each part of the program means the correctness of the entire program. Dafny requires some unique tools to support formal verification. The terms of related keywords and other keywords are shown in Table 1.
Dafny uses a syntax similar to other programming languages, but it requires some special tools to help with formal verification. Annotation is a tool provided by Dafny to help users verify the program. Annotation is not part of the actual program, but it provides specifications and information about methods in the program. By considering the annotations in the function, Dafny can more directly verify the correctness of the program. Dafny transforms the burden of writing bugfree code into the burden of writing bugfree annotations. It is usually easier than writing code, because annotations are shorter and more direct. In addition, the behavior of writing annotations can help people understand what the code does at a deeper level. Dafny can also prove that there are no runtime errors, such as index out of bounds, null cancellation, division by zero, etc.
An overview of the entire Dafny system is given in Fig. 1. The way programmers interact with it is the same as static type checker, when the tool reports an error, the programmer will respond by changing the program’s type declaration, specifications, and statements. After the Dafny code passes the Dafny compiler, there are two paths: one is that the Dafny compiler directly generates C # code, and then compiles it to the MSIL byte code of the .NET platform; the other is that Dafny’s program verifier converts the given Dafny program into the intermediate verification language Boogie^{[22]}. Then, the Boogie tool generates a firstorder verification condition, and finally passes it to the Z3^{[23]} SMT solver^{[24]} for verification. Any content that violates these conditions will be returned as a verification error.
Fig.1 Verification mechanism diagram
Verification mechanism diagram 
Keywords table
3 Deductive Synthesis of Dafny Programs for Two Typical Problems
In this section, we will use the deductive and synthesis method to develop Dafny programs^{[25]} for two typical problems. One is the minimum contiguous subarray problem; another is the new local bubble sorting problem.
3.1 Minimum Contiguous Subarray
Problem description: Calculate the minimum sum of
adjacent elements in a given integer array a[0: n1].
● Provide problem specification
Using minsum(n1) to represent the smallest sum of contiguous subarray of its input array a[0: n1].
Q: n>0
R: minsum(n1) = (MIN i, j:0≤i≤j<n:sum(i, j))
The auxiliary function sum (i, j) is defined as follows:
sum(i,j)= (∑k:i≤k≤j: a[k])=sum(i, j1)+a[j1], i≤j
sum(i,j)=0, if i>j
The auxiliary function min is defined as follows:
min(a,b)= if a>b then b else a
● Partition the original problem
Divide the original problem into subproblems with the same structure, then construct a recursive relationship for solving the problem and a preliminary algorithm. Obviously, the most commonly used method for this problem is the exhaustive method. That is to list the sum of all adjacent elements and compare them to get the solution of the minimum contiguous subarray program, and the time complexity of the algorithm is O(n ^{3}). But, we derive another algorithm to reduce the time complexity and optimize the algorithm. We divide the original problem as follows:
minsum(a[0:n1])=F(minsum(a[0:m2],a[m1])), 0≤m≤n
We start with the postassertion to find the recursive relationship F.
● Find the recurrence relations
minsum(a[0:m])
=(MIN i, j : 0≤i≤j≤m: sum(i,j))
=[crossproduct nature]
(MIN j:0≤j≤m: (MIN i: 0≤i≤j: sum(i, j)))
=(MIN j:0≤j≤m: ms(j)))
Define ms (j) = (MIN i: 0≤i≤j: sum (i, j))
=min((MIN j: 0≤j≤m: ms(j))), ms(m))
=[range division and single range]
=min(minsum(a[0: m1]), ms(m))
The first recursive relationship is:
Recurrence1:
minsum(a[0:m])=min(minsum(a[0:m1]),ms(m)), 0≤m≤n
Because Recurrence 1 contains the function of ms (m), we need to find the relationship between ms (m) and ms (m1):
ms(m)
=(MIN i:0≤i≤m:sum(i,m))
=(MIN i:0≤i≤m: (∑k:i≤k≤m:a[k]))
=[range division and single range]
=(MIN i:0≤i≤m: (∑k:i≤k≤m1:a[k])+ a[m])
=[General distribution law and Definition of sum]
=(MIN i: 0≤i≤m:sum(i,m1))+a[m]
=[range division and single range]
=min((MIN i:0≤i<m:sum(i,m1)), sum(m, m1)) a[m]
=[Definition of ms(m)]
=min(ms(m1),0)+a[m]
=min(ms(m1)+a[m],a[m])
The second recursive relationship is:
Recurrence 2:
ms(m)=min(ms(m1)+a[m], a[m])
When m = 0, ms(m1) = 0, minsum(a [0: m1]) = 0, we can get Initialization 1.
Initialization 1: m = 0 ∧ ms(m1)=0 ∧ minsum (a [0: n1]) = 0.
● Write the loop invariant
We can get the loop invariant by storing minsum (a[0:m1]) and ms(m) into the variable s and c.
ρ : 0≤m≤n∧s= minsum(a[0:m1])∧c=ms(m)
● Generate the Dafny algorithm program
Then, the algorithm with time complexity of O(n) is obtained by combining the Initiation 1, Recurrence 1 and Recurrence 2. Compared with time complexity O(n ^{3}) of the exhaustive method, the algorithm has better optimization efficiency. Algorithm program is as follows:
method minsum(a: array〈int〉) returns(s: int)
{
var m , c := 0 , 0; s := 0;
while(m<a.Length)
decreases a.Lengthm
{
c := min(c + a[m],a[m]);
s := min(s, c);
m := m + 1;
}
}
The Q, R, auxiliary functions in the first step, and the loop invariant in the fourth step are respectively expressed by Dafny and added to the Dafny program for verification. The Dafny program for the smallest sum of contiguous subarrays is as follows:
function method sum(a: array〈int〉, i: int, j: int): int
reads a
requires a!= null
requires 0≤i≤j≤a.Length
decreases ji
{
if j == i then 0 else sum(a, i, j  1) + a[j1]
}
function method min(a:int, b:int):int
{if a>b then b else a}
method minsum (a: array 〈int〉) returns(s: int)
requires a != null
ensures for all i, j :: 0≤i<j≤a.Length1 ==> sum(a, i, j) >= s
{
var m , c := 0 , 0; s := 0;
while(m<a.Length)
invariant 0≤m≤a.Length
invariant for all i, j :: 0≤i<j≤m ==>sum(a, i, j) >= s
invariant for all i :: 0≤i<m ==> sum(a, i, m) >= c
decreases a.Lengthm
{
c := min(c + a[m],a[m]);
s := min(s, c);
m := m + 1;
}
}
● Verification of the final Dafny algorithm program
The following are the main methods and verification results of minsum (Fig. 2).
method Main()
{
var a:array<int>:= new int[7][4,7,6,3,9,1,2];
var m := minsum(a);
print "minsum:", m;
}
Fig.2 Minsum verification result
Minsum verification result 
3.2 New Local Bubble Sorting
Problem description: Arrange the given integer array a [0: n1] in no descending order.
● Provide problem specification
Using BubbleSort(a,0,n) to represent the postconditions of Bubble Sort.
Q: a != null & n>0
R: BubbleSort(a,0,n) = (∀j : 1≤j<n : a[j1]≤a[j]) ∧perm(a,b,0,n1)
The auxiliary function perm(a,b,0,n1) is defined as follows:
perm(a,b,0,n1)≡(∀i:0≤i<n: (Nj: 0≤j<n:a[j] =a[i]) =(Nk: 0≤k<n:b[k]=a[i]))
● Partition the original problem
Dividing the original problem into subproblems with the same structure, constructing a recursive relationship for solving the problem and a preliminary algorithm.
BubbleSort(a, m, n)=F(BubbleSort(a, m+1, n), BubbleStep(a, m, n)), 0≤m≤n
We start with the postassertion to find the recursive relationship F.
● Find the recurrence relations
Dividing the original problem and finding the recursive relationship. Defining partition function through constructing subproblems.
BubbleSort(a , m , n)
=( ∀j:m≤j<n: a[j1]≤a[j])
=(∀i , j:m≤j≤i<n:a[j1]≤a[j])
=(∀i , j:m≤j<n∧m≤i<n:a[j1]≤a[j])
=[crossproduct nature]
=(∀i:m≤i<n:(∀j:m≤j<n:a[j1]≤a[j]))
=(∀i:m+1≤i<n:(∀j:m≤j<n:a[j1]≤a[j]) )
∧(∀j:m≤j<n:a[j1]≤a[j]))
=[range division and single range]
=BubbleSort(a, m+1, n)∧(∀j: m≤j<n: a[j1]≤a[j]))
=[Definition of BubbleSort]
Letting BubbleStep (a, m, n) = (∀j: m≤j<n: a[j1] ≤a[j])), we get the first recursive relation of bubble sorting algorithm.
1BubblesortUp:BubbleSort(a,m,n)=BubbleSort(a,m+1,n)∧BubbleStep(a,m,n), m:1..n
The following is the recursive relationship of the BubbleStep function.
BubbleStep(a, m, j)
=(∀k:m≤k≤j1:a[k1]≤a[k])
=[restricted variable name change, definition]
=(∀k:m≤k≤j2:a[k1]≤a[k])∧a[j1]≤a[j]
=[range division and single range]
=bubbleStep(a ,m , j1)∧a[j1]≤a[j]
We can get the second recursion relation from right to left.
2BubbleStepRL:
BubbleStep(a, m, j)=BubbleStep(a,m,j1)∧a[j1]≤a[j], j:m..1
Combining the recursive relations 1, 2 and changing the name of the variable m to i, we obtain the following two recursive relations.
BubbleSort(a,i,n) =BubbleSort(a,i+1,n)∧BubbleStep(a,i,n), i:1..n
BubbleStep(a,i,j)=BubbleStep(a,i,j1)∧a[j1]
≤a [j], j:i..1
● Write the loop invariant
Combining the definitions of the recursive relation BubbleSort and BubbleStep and the variable scope of i , j. we can obtain the loop invariant:
ρ : BubbleSort(a, i, n)=(∀i:m+1≤i<n:(∀j:m≤j<n:a[j1]≤a[j]))∧BubbleStep(a,i,j1)=∧a[j1]≤a[j]; i: 1..n, j:i..1
● Generate the Dafny algorithm program
Here are two Dafny methods to achieve the above recursive relationship:
method BubbleSort(a:array〈int〉)
{
if a.Length>1
{
var i := 1;
while i<a.Length
decreases a.Lengthi;
{
BubbleStep (a , i);
i := i + 1;
}
}
}
method BubbleStep (a:array〈int〉, i:int )
{
var j := i;
while (j>0 && a[j1]>a[j])
decreases j
{
a[j1],a[j] := a[j], a[j1];
j := j1;
}
}
Add Q, R, auxiliary functions, and loop invariants to Dafny methods for verify:
predicate permutation (a: seq〈int〉,b: seq〈int〉)
{
multiset (a) == multiset (b)
}
predicate ord(a: array〈int〉, lo : int , hi : int )
requires a != null && 0 <= lo <= hi <= a . Length
reads a
{
For all i, j ::lo <= i < j < hi ==> a[i] <= a[j]
}
predicate sorted (a: array〈int〉)
requires a != null
reads a
{
ord(a ,0, a.Length)
}
method bubbleSort(a:array〈int〉)
requires a != null
modifies a
ensures sorted(a)
ensures permutation (a[..] , ord (a[..]))
{
if a.Length>1
{
var i := 1;
while i<a.Length
invariant 1<= i <= a.Length;
invariant ord(a,0,i);
invariant permutation (a[..], ord(a[..]));
decreases a.Lengthi;
{
bubbleStep (a , i);
i := i + 1;
}
}
}
method BubbleStep (a:array〈int〉, i:int )
requires a != null && 0 <= i<a.Length && ord(a ,0 , i )
modifies a
ensures ord(a ,0 , i+1)
ensures permutation (a[..] , ord (a[..]))
{
var j := i;
while (j>0 && a[j1]>a[j])
invariant 0 <= j <= i && ord (a ,0 , j ) && ord(a, j , i+1)
invariant 1<j+1 <= i ==> a[j1]<= a[j+1]
invariant permutation (a[..], ord(a[..] ))
decreases j
{
a[j1],a[j]:= a[j],a[j1];
j:= j1;
}
}
● Verification of the final Dafny algorithm program
The following are the main method and verification results of the BubbleSort (Fig.3).
method Main()
{
var a:array〈int〉 := new int[7] [4, 0, 1, 9, 7, 1, 2];
print "Before: ", a[0], a[1], a[2], a[3], a[4], a[5], a[6], "\n";
BubbleSort(a);
print "After: ", a[0], a[1], a[2], a[3], a[4], a[5], a[6], "\n";
}
Fig.3 BubbleSort verification result
BubbleSort verification result 
4 Conclusion
In this paper, we propose a system method to deduce and synthesize the Dafny programs. First, the specification of problem is described in strict mathematical language. Then, the derivation process uses program specification transformation technology to perform equivalent transformation. Furthermore, Dafny program is synthesized through the obtained recursive relationship and loop invariants. Finally, the functional correctness of Dafny program is automatically verified by Dafny verifier or online tool. Through this method, we deduce and synthesize Dafny programs for many typical problems such as the cube sum problem, the minimum (or maximum) contiguous subarray problems, several searching problems, several sorting problems. Due to space limitation, we only illustrate the development process of Dafny programs for two typical problems: the minimum contiguous subarray problem and the new local bubble sorting problem. It proves that our method can effectively improve the correctness and reliability of Dafny program developed. What’s more, we demonstrate the potential of the deductive synthesis method by developing a new local bubble sorting program.
Our next plan is to use this method and combine with our previous work^{[2631]} to deduce and synthesize more complex nonlinear data structure algorithms, such as the binary tree or graph related algorithms.
References
 Leino K R. Accessible software verification with Dafny [J]. IEEE Software , 2017, 34 (6): 9497. [Google Scholar]
 Leino K R. Dafny: An automatic program verifier for functional correctness [C]// International Conference on Logic Programming .Berlin: SpringerVerlag, 2010: 348370. [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]
 Leino K R, Monahan R. Dafny meets the verification benchmarks challenge [C]// Verified Software Theories Tools Experiments . Berlin: SpringerVerlag, 2010: 112126. [CrossRef] [Google Scholar]
 Burstall R M, Darlington J. A transformation system for developing recursive programs [J]. Journal of the ACM , 1977, 24 (1): 4467. [Google Scholar]
 Visser E. A survey of strategies in rulebased program transformation systems [J]. Journal of Symbolic Computation , 2005, 40 (1): 831873. [CrossRef] [MathSciNet] [Google Scholar]
 Balog M, Gaunt A L, Brockschmidt M, et al . DeepCoder: Learning to write programs [C]// Proceedings of International Conference on Learning Representations . Washington D C : IEEE, 2017: 121. [Google Scholar]
 Bornholt J, Torlak E. Synthesizing memory models from framework sketches and litmus tests [J]. ACM SIGPLAN Notices , 2017, 52 (6): 467481. [CrossRef] [Google Scholar]
 Brockschmidt M, Allamanis M, Gaunt A. Generative code modeling with graphs [C]// Proceedings of International Conference on Learning Representations . Louisiana: ICLR, 2019: 124. [Google Scholar]
 Exlcovisser. Programtransformation.org [EB/OL]. [2007 0214]. http://www.programtransformation.org . [Google Scholar]
 Pettorossi A, Proietti M. Automatic derivation of logic programs by transformation [J]. Course Notes for European Summer School on Logic, Language, and Information , 2000, 45 (1): 187. [Google Scholar]
 Secher J P. Unfold/Fold transformation, graduate course of university of copenhagen [EB/OL]. [20010212]. http://www.diku.dk/topps/activities/pgmtrans/unfoldfold.ps . [Google Scholar]
 Pettorossi A, Proietti M. Program derivation = rules + strategies [C]// Computational Logic: Logic Programming and Beyond (Essays in Honour of Robert A. KowalskiPart I) . Berlin: SpringerVerlag, 2002: 273309. [Google Scholar]
 Morgan C. Programming from Specifications [M]. Oxford: Oxford University Press, 1991. [Google Scholar]
 Pavlovic D, Smith D R. Software development by refinement [C]// Formal Methods at the Crossroads: From Panaea to Foundational Support, LNCS . Berlin: SpringerVerlag, 2003: 267286. [Google Scholar]
 Wang X, Dillig I, Singh R. Program synthesis using abstraction refinement [J]. Proceedings of the ACM on Programming Languages , 2017, 45 (2): 131. [Google Scholar]
 Leavens G T, Abrial J R, Batory D. Roadmap for enhanced languages and methods to aid verification [C]// 5th Int’l Conf on Generative Programming and Component Engineering . Philadelphia: ACM Press, 2006: 221236. [CrossRef] [Google Scholar]
 Xue J Y, You Z, Hu Q. PAR: A practicable formal method and its supporting platform [C]// International Conference on Formal Engineering Methods . Berlin: SpringerVerlag. 2018: 7086. [Google Scholar]
 You Z, Xue J Y. Formal verification of algorithmic programs based on the Isabelle theorem prover [J]. Computer Engineering and Science , 2009, 31 (10): 8589(Ch). [NASA ADS] [Google Scholar]
 Barnett M, Leino K R M, Schulte W. The spec# programming system: An overview [C]// International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices . Berlin: SpringerVerlag, 2004: 120. [Google Scholar]
 Fisler K, Krishnamurthi S. Modular verification of collaborationbased software designs [C]// European Software Engineering Conference; ESEC; ACM SIGSOFT Symposium on the Foundations of Software Engineering; FSE9 . Washington D C: IEEE, 2001: 1014. [Google Scholar]
 Barnett M, Chang B E, Deline R, et al . Boogie: A modular reusable verifier for objectoriented programs [C]// 4th International Symposium Lecture Notes in Computer Science , Berlin: SpringerVerlag, 2006: 364387. [CrossRef] [Google Scholar]
 Moura L D, Bjorner N. Z3: An efficient SMT solver [C]// Tools and Algorithms for Construction and Analysis of Systems . Berlin: SpringerVerlag, 2008: 337340. [Google Scholar]
 Leino K R. Automating induction with an SMT solver [C]// Proc 13th Int’l Conf Verification, Model Checking, and Abstract Interpretation . Berlin: SpringerVerlag, 2012: 315331. [CrossRef] [MathSciNet] [Google Scholar]
 Hu Q M, Xue J Y, You Z, et al . Research on the formal verification technology of several software components in the PAR platform [J]. Computer Engineering and Science , 2018, 40 (2): 268274(Ch). [Google Scholar]
 Wang C J, He J F, Luo H M, et al . Modeldriven formal generation and automatic validation of Dafny programs [J]. Journal of Jiangxi Normal University , 2020, 44 (4): 378384(Ch). [Google Scholar]
 Wang C J, Yu X J, Shen D M, et al .A twolayer verification method for concurrent distributed shared memory algorithm based on concurrent Apla [J]. Journal of Jiangxi Normal University , 2020, 44 (3): 301306(Ch). [Google Scholar]
 Zuo Z K, Fang Y, Huang Q, et al .Nonrecursive binary tree sorting algorithm and its formal proof [J]. Journal of Jiangxi Normal University , 2020, 44 (6): 6256329(Ch). [Google Scholar]
 Zuo Z K, Lu Z H, Huang Q, et al . A comparative study of generic features between Apla and programming languages [J]. Journal of Jiangxi Normal University , 2019, 43 (5): 454461(Ch). [Google Scholar]
 Zhou W X, Zuo Z K, WANG C J, et al . The contrastive study of generic programming in objectoriented languages [J]. Journal of Jiangxi Normal University , 2018, 42 (3): 304310(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 , 2018, 42 (3): 29830(Ch). [Google Scholar]
All Tables
All Figures
Fig.1 Verification mechanism diagram
Verification mechanism diagram 

In the text 
Fig.2 Minsum verification result
Minsum verification result 

In the text 
Fig.3 BubbleSort verification result
BubbleSort verification result 

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.