© Wuhan University 2021

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 well-designed 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 high-level expressions of user intent^[5-7] in the past decade. Some of these techniques are geared towards computer end-users and they utilize informal specifications such as input-output 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 semi-formal 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^[8-10]. 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^[11-13] to get better transform rules.

Program refinement ^[14]. At present, some good program refinement work has been applied to practice. The authors of Refs.[15-17] 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) Cross-product 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 object-based programming paradigms. It supports generic classes and dynamic allocation, with built-in 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 pre-conditions and post-conditions, framing specifications (reads and modifies sets), loop invariants, and termination metrics. To further support the specification, the language also provides updatable ghost variables, user-defined 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 bug-free code into the burden of writing bug-free 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 first-order 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

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: n-1].

● Provide problem specification

Using minsum(n-1) to represent the smallest sum of contiguous subarray of its input array a[0: n-1].

Q: n>0

R: minsum(n-1) = (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, j-1)+a[j-1], 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 sub-problems 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 ³). But, we derive another algorithm to reduce the time complexity and optimize the algorithm. We divide the original problem as follows:

minsum(a[0:n-1])=F(minsum(a[0:m-2],a[m-1])), 0≤m≤n

We start with the post-assertion to find the recursive relationship F.

● Find the recurrence relations

minsum(a[0:m])

=(MIN i, j : 0≤i≤j≤m: sum(i,j))

=[cross-product 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: m-1]), ms(m))

The first recursive relationship is:

Recurrence1:

minsum(a[0:m])=min(minsum(a[0:m-1]),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 (m-1):

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≤m-1:a[k])+ a[m])

=[General distribution law and Definition of sum]

=(MIN i: 0≤i≤m:sum(i,m-1))+a[m]

=[range division and single range]

=min((MIN i:0≤i<m:sum(i,m-1)), sum(m, m-1)) a[m]

=[Definition of ms(m)]

=min(ms(m-1),0)+a[m]

=min(ms(m-1)+a[m],a[m])

The second recursive relationship is:

Recurrence 2:

ms(m)=min(ms(m-1)+a[m], a[m])

When m = 0, ms(m-1) = 0, minsum(a [0: m-1]) = 0, we can get Initialization 1.

Initialization 1: m = 0 ∧ ms(m-1)=0 ∧ minsum (a [0: n-1]) = 0.

● Write the loop invariant

We can get the loop invariant by storing minsum (a[0:m-1]) and ms(m) into the variable s and c.

ρ : 0≤m≤n∧s= minsum(a[0:m-1])∧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 ³) 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.Length-m

  {

   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 j-i

 {

  if j == i then 0 else sum(a, i, j - 1) + a[j-1]

 }

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.Length-1 ==> 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.Length-m

  {

    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

3.2 New Local Bubble Sorting

Problem description: Arrange the given integer array a [0: n-1] in no descending order.

● Provide problem specification

Using BubbleSort(a,0,n) to represent the post-conditions of Bubble Sort.

Q: a != null & n>0

R: BubbleSort(a,0,n) = (∀j : 1≤j<n : a[j-1]≤a[j]) ∧perm(a,b,0,n-1)

The auxiliary function perm(a,b,0,n-1) is defined as follows:

perm(a,b,0,n-1)≡(∀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 sub-problems 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 post-assertion to find the recursive relationship F.

● Find the recurrence relations

Dividing the original problem and finding the recursive relationship. Defining partition function through constructing sub-problems.

BubbleSort(a , m , n)

=( ∀j:m≤j<n: a[j-1]≤a[j])

=(∀i , j:m≤j≤i<n:a[j-1]≤a[j])

=(∀i , j:m≤j<n∧m≤i<n:a[j-1]≤a[j])

=[cross-product nature]

=(∀i:m≤i<n:(∀j:m≤j<n:a[j-1]≤a[j]))

=(∀i:m+1≤i<n:(∀j:m≤j<n:a[j-1]≤a[j]) )

∧(∀j:m≤j<n:a[j-1]≤a[j]))

=[range division and single range]

=BubbleSort(a, m+1, n)∧(∀j: m≤j<n: a[j-1]≤a[j]))

=[Definition of BubbleSort]

Letting BubbleStep (a, m, n) = (∀j: m≤j<n: a[j-1] ≤a[j])), we get the first recursive relation of bubble sorting algorithm.

1-BubblesortUp: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≤j-1:a[k-1]≤a[k])

=[restricted variable name change, definition]

=(∀k:m≤k≤j-2:a[k-1]≤a[k])∧a[j-1]≤a[j]

=[range division and single range]

=bubbleStep(a ,m , j-1)∧a[j-1]≤a[j]

We can get the second recursion relation from right to left.

2-BubbleStepRL:

BubbleStep(a, m, j)=BubbleStep(a,m,j-1)∧a[j-1]≤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,j-1)∧a[j-1]

≤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[j-1]≤a[j]))∧BubbleStep(a,i,j-1)=∧a[j-1]≤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.Length-i;

  {

   BubbleStep (a , i);

    i := i + 1;

  }

 }

}

method BubbleStep (a:array〈int〉, i:int )

{

 var j := i;

  while (j>0 && a[j-1]>a[j])

  decreases j

  {

    a[j-1],a[j] := a[j], a[j-1];

    j := j-1;

  }

}

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.Length-i;

   {

    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[j-1]>a[j])

 invariant 0 <= j <= i && ord (a ,0 , j ) && ord(a, j , i+1)

 invariant 1<j+1 <= i ==> a[j-1]<= a[j+1]

 invariant permutation (a[..], ord(a[..] ))

 decreases j

 {

   a[j-1],a[j]:= a[j],a[j-1];

   j:= j-1;

 }

}

● 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

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^[26-31] to deduce and synthesize more complex nonlinear data structure algorithms, such as the binary tree or graph related algorithms.

References

All Tables

All Figures

	Fig.1 Verification mechanism diagram
In the text

	Fig.2 Minsum verification result
In the text

	Fig.3 BubbleSort verification result
In the text