Abstract: Software testing can find errors, but can not find them absent. Because program verification can provide this guarantee, it has arguably been one of the most fertile application areas of formal methods and becomes more and more important in software development. Proving the correctness of a program entails showing that if the program is initiated from a machine state satisfying a certain precondition then the state on termination satisfies some desired post-condition. The emphasis was put on formal verification in program proving previous. If we can algebraize program proving, the correctness proving can be mechanized and automated easily and the efficiency of proving can be also improved greatly. Wu’s method has been shown to improve efficiencies in mechanical geometry theorem proving, where it can replace the well-known Grobner basis method. It seems to have promise to bring the powerful mathematical machinery to settle the program total correctness problem. This study applies Wu’s characteristic set method and mathematical induction to proving the total correctness of recursive program. Our method is based on the algebraic theory of polynomial set, which have wider application domain. We implement this method with the computer algebra tools MMP. The application of the method is demonstrated on a few examples. Compared with proving tool Isabelle, our method is more efficient through experiments and greatly improves the efficiency of proving especially in polynomial program. In this way, an algebraic approach based on mathematics mechanization is introduced to software verification. A new idea for program correctness proving is proposed in this study.
INTRODUCTION
Testing is becoming one of the key-aspects of software development methodologies. Usually, methods for program correctness proving are testing. They can find errors but cannot cover all bugs. Formal verification approaches, e.g., formal program correctness proving, can provide this guarantee (Mao and Wu, 2005). As software development with reuse is seen as one of the most important factors, formal verification becomes a very attractive approach to the perfect development of software systems for the reusable component should be completely correct. Since Floyd-Hoare-Dijkstras inductive assertion method using pre/post-conditions was proposed in the late sixties for verifying properties of imperative programs, the success however has been limited. Recently, due to the advance of computer algebra, several methods based on symbolic computation can be applied successfully to program correctness proving.
Wu’s algorithm is an efficient method for solving systems of polynomial equations, which mainly calculates a characteristic set of a finite set of polynomials. It is especially relevant in the framework of algorithmic geometry, where it can replace the well-known Grobner basis method. Also, it seems to have promise to bring the powerful mathematical machinery to settle the program total correctness problem. In fact many programs or program fragments (They should include assignment statements which can be transformed into transition equations. Each assignment state is like x = e where e is an expression. It can also be transformed into the transition equation like x - e = 0.) can be represented as algebraic transition systems (Sankaranarayanan et al., 2004) and transitions between program states can be represented as polynomial equations. Once program can be algebraized, the correctness proving can be mechanized and automated easily and the efficiency of proving can be also improved greatly.
Total correctness of programs means two things: termination and partial correctness with respect to a specification. This study introduces an approach of polynomial algebra to prove program correctness, shows Wu’s method can be applied to program correctness proving and proposes a method based on mathematics mechanization to verify correctness of recursive program. Wu’s method is an algorithm of representing the zeros of a set of polynomials with the characteristic sets and we can use Wu’s method to prove recursive program correctness by calculating the characteristic set. Our method can be more efficient and implemented on computer easily and mechanically and presents a new idea for proving the total correctness of program. It is a polynomial algebraic method and polynomial algebraic method is different from classical logical method because the latter emphasizes on logical reasoning and the former emphasizes on computation.
Some work has been proposed to recursive program correctness proving. Krauss (2006) developed an automated tool for defining partial recursive functions in Higher-Order Logic and providing appropriate reasoning tools for them. He implemented his tool as a definitional specification mechanism for Isabelle/HOL (http://www.isabelle.in.tum.de/). Popov and Jebelean (2009) describe an innovative method for proving the total correctness of tail recursive programs having a specific structure.
Wu’s method: Wu’s method is an efficient method in symbolic computation, which finds zeros of a set of polynomials by looking for the characteristic sets. Roughly speaking, one would like to obtain a triangular base B of S, i.e., a sequence of polynomials (pi, . . . , pm) such that every polynomial in S is a linear combination of polynomials in B. In this section, we give a brief review of the necessary results in the theory of Wu’s method and (Wu, 2001) for a detailed exposition.
We first give some notational conventions, which are also directly useful for our purpose of proving program correctness. Let, K[x1, . . . , xn] be the ring of polynomials in n variables over a field K. For the sake of simplicity, K is supposed to be an algebraically closed field. Let degxj(f) be the maximum degree of the variable xj in the polynomials f ∈ K[x1, . . . , xn]. Let G =< g1, . . . , gr > be a finite sequence of polynomials g1, . . . , gr ∈ K[x1, . . . , xn]. In the following, all the polynomials mentioned are in K[x1, . . . , xn]. A fixed ordering on the set of variables is considered. Without loss of generality, we assume that the given variables ordering is:
| (1) |
Definition 1: Given a polynomial:
| (2) |
Its initial polynomial, In(f) is defined to be the polynomial Id(x1,...,xj-1). We use In(P) in the following to denote the set of the initial polynomials in P:
| (3) |
Definition 2: A variable xj is said to be in f if some monomial in f with nonzero coefficient contains a positive power of xj. If xj is in f and no variable xi with xi ™ xj is in f, then:
| (4) |
If no variables exist in f, then class(f) = 0 and cdeg(f) = 0.
Definition 3: We say that f is of lower rank than g, if either:
| (5) |
The basic idea of Wu’s algorithm is to enlarge the initial set S with
new polynomials obtained by a certain pseudo-division procedure. Let p be a
polynomial in K[x1, . . . , xn]. The partial degree of
p with respect to the variable xi is denoted degxj(p).
The head variable of p is the variable xc, occurring in p with maximal
c and, in this case, c is called the class of p; the initial polynomial In(p)
of p is the coefficient of
Theorem 1: For any two polynomials f and g with class(f) = j., there exist a non-negative number α and polynomials q and r, such that:
| (6) |
where,
|
|
If r = g, then g is said to be reduced with respect to f and r is denoted by prem(g, f, xj) as usual (prem is abbreviation of pseudo-remainder).
Definition 4: G is said to be an ascending set, if one of the following two conditions holds:
| • | r = 1 and g1 is not equal to zero |
| • | r > 1 and 0 < class(g1) < class(g2) < … <class(gr) ≤ n and each gi is reduced with respect to each of the preceding polynomials gj(1≤ j < i) |
Considering an ascending set G, a polynomial f and using pseudo-division successively:
| (7) |
We obtain:
where,
The remainder r0 is usually denoted by prem(f, G).
Definition 5: The ascending set G is a characteristic set of P if and only if:
| (8) |
From the above definition, we can present an algorithm on how to compute a characteristic set of a set of polynomials. We call an algorithm to compute a characteristic set of a set of polynomials Wu’s method. The algorithm can be modified in various ways for better performance. However, the common algorithm in Wu’s method is doing pseudo-division successively, with respect to an ascending set. It adds the remainders to the set of polynomials successively until all the remainders are 0.
Definition 6: We use Zero(S) to denote the zero set of S:
| (9) |
Theorem 2: Let, B be a characteristic set of S. Then:
| (10) |
Theorem 3: Given each Pi∪B, we calculate the corresponding characteristic set by using Wu’s method. Let, {Bi, 1≤i≤μ} be all the characteristic sets obtained that include B and have:
| (11) |
In a word, the essence of Wu’s method is that we can obtain:
and Wu’s characteristic set {g1, g2, . . . , gt, r0} through pseudo-division if:
gi = 0 and r0 = 0 then:
f = hg = 0 and Zero(f) = Zero(p)/Zero(h), where:
In this way, we can obtain a characteristic set of a set of polynomials.
APPLICATION OF WU’S METHOD TO VERIFYING CORRECTNESS OF RECURSIVE PROGRAM
In geometric proving we algebraize the proposition (conclusion or conjectures) which need to be proved and the given conditions (or hypotheses) firstly. Suppose that the algebraized conclusion is p and the algebraized given conditions (or hypotheses) are S = {f1 = 0, f2 =0, ..., fs = 0}. Then we set p as goal and set S={f1 =0, f2 = 0, ... , fs = 0} as constraint conditions. From the hypothesis (constraint condition) polynomials we compute a set of polynomials in a triangular form called Wu's characteristic set B = (g1 = 0, …, gt = 0) which every polynomial in S is a linear combination of polynomials in B, namely fi ∈S and:
Next we check whether the conclusion polynomial p pseudo-divides to 0 using the polynomials in the characteristic set, namely we use every element of the characteristic set pseudo-divide the conclusion p to obtain pseudo-remainder r.
Then, we know there should be:
If r0 = 0 and
then we can draw a conclusion p = 0. Characteristic sets are computed using pseudo-division by introducing a total ordering on dependent variables. The inequations:
have been called nondegenerate conditions or subsidiary conditions in the literature (Mao and Wu, 2005).
Hypothesize that r0 is terminate polynomial assertion when the program terminates. If r0 = 0, namely r0 satisfies termination condition and state transition equations or constraint conditions f1 = 0, . . . , fs = 0, then the program will terminate and we will deduce that the inductive polynomial assertion p = 0 is true.
According the above discussion, we can apply Wu's method to verifying correctness of recursive program and formalize our method as follow.
Suppose that recursive program is P. Extract termination condition, state transition equations (constraint conditions) and goal from recursive program and triangularize state transition equations.
Termination condition:
| (12) |
Goal or conclusion:
| (13) |
State transition equations (constraint conditions):
| (14) |
where u1,u2,...,ur are independent parameters and x1,...,xs are dependent parameters.
We triangularize state transition equations (constraint conditions) and obtain:
| (15) |
Assume that the given variables’ ordering (We must give variables’ ordering in advance. Wu’s method is an elimination method and the variables’ ordering can point out the elimination sequence of variables. For example when we eliminate variable xi the given ordering guarantees that variable whose order greater than xi will not recur in computing. Otherwise, the computation which finds the characteristic set does not terminate.), find loop invariants of recursive program and relation formulae among states and prove that the sequence of states forms a descending chain and there exists states which satisfy termination condition and lay a foundation for induction. If the corresponding relation formulae among certain states have been reduced with state transition equations but the states do not satisfy termination condition, then the program will not terminate.
Assume the induction hypothesis and apply Wu’s method and mathematical induction to proving partial correctness of the recursive program. If the termination and partial correctness of the program are proved, then the program is totally correct.
According to Cao and Zhu (2010) we obtain the loop invariant L(x1, x2, …, xs) of recursive program P. Suppose xs is a output variable and x1, x2, …, xs-1 are input variables and by loop invariant L(x1, x2, …, xs) we compute the relation formula:
| (16) |
which is between input variables and output variable in each recursion. Assume
there exist n recursions in P and when n = 1 we compute whether xs
= H (x1, x2, …, xs-1) satisfies termination
condition namely we compute program state
is true and the hypothesis need to be proved is:
We use I to be divided by f*1, f*2,...,f*s to obtain:
| (17) |
According to the induction hypothesis:
and constraint conditions f*1, f*2,...,f*s we find out whether Rn is 0. If Rn =0 then I=0 and we know that the program is partially correct. Because termination of the program has already been proved:
total correctness of the recursive program is proved.
We demonstrate how to apply Wu's method to recursive program correctness proving by using Euclid's algorithm (gcd: greatest common divisor) example. The Example 1 (Hu et al., 2003) will be described as follow:
| (18) |
At first, we compute an invariant of recursion according to (Cao and Zhu, 2010).
| (19) |
r, s ∈ Z and x* and y* are initial values of x and y.
The iterative calls of recursive program produce a sequence of arguments or states xn = x*, yn = y*, xn-1, yn-1, … Termination condition, state transition equations (constraint conditions) and goal will be described as algebraic formulae as follow:
We give termination condition according to exit condition of recursion and output value at exit.
| (20) |
State transition equations (constraint conditions):
| (21) |
| (22) |
Goal:
| (23) |
We assume that the given variables’ ordering is
| (24) |
In order to use pseudo-division correctly, we should triangularize state transition equations. Equation 21 and 22 will be transformed into:
| (25) |
| (26) |
We start to use pseudo-division to calculate Wu’s characteristic set. There exists F = rnxn + snyn - z = 0, where xn = x* and yn = y*. If yn < xn, we use F to be divided by f*1 to obtain:
| (27) |
We use R'n to be divided by f*2 to obtain:
| (28) |
Let rn-1 = sn and sn-1 = rn, Rn = rn-1xn-1 +sn-1yn-1 - z = 0.
If yn≥ xn, we use F to be divided by f*3 to obtain:
| (29) |
We use R'n to be divided by f*4 to obtain:
| (30) |
Let rn-1 = rn-1+sn and sn-1 = sn, Rn = rn-1xn-1 +sn-1yn-1 - z = 0.
We apply pseudo-division to Rn (we substitute n-1 for subscript n and substitute n-2 for subscript n-1 in f*1, f*2, f*3 and f*4 here) and repeat to apply pseudo-division to calculating pseudo-remainder. There exists:
| (31) |
In this way, we obtain a Wu’s characteristic set {f*1, f*2, . . ., R2}. If xn, xn-1, xn-2, . . . form a descending chain (we will prove it later) and there should exist xm = 0 which satisfies termination condition and
| (32) |
when xm = 0, the program will terminate and z =smym. If sm = 1 and m = 1, R2 = y1 - z = 0 and z =y1 = GCD(0, y1), namely z is output variable value.
Suppose that the relation formula between input variable values xn and yn and output variable value z or the relation formula among program states is:
| (33) |
According the above discussion, we can verify correctness of recursive program GCD by applying Wu’s method and mathematical induction.
Proof: First we prove termination of recursive program and lay a foundation for induction.
If x1 = 0 and y1 > 0, then x1 = 0 satisfies termination condition and y1 - z = 0 satisfies the relation between input variables xn and yn and output value z. Here, the program will terminate and output variable value z = GCD(0, y1) = y1.
If y2 = 0 and x2 > 0, then because y2 < x2, we use F = x2-z to be divided by f*1 = x2-y1 = 0 and f*2 =y2-x1 = 0 to obtain R2 = y1-z = 0 and x1 = 0 which satisfies termination condition. Therefore we obtain Wu’s characteristic set {f*1, f*2, R2} and F = f*1+0•f*2+R2. Similarly the program will terminate and output variable value z = y1.
If xi > 0 and yi > 0, then we calculate by using state transition equations. If yi < xi, then xi-1 = yi <xi. The chain xn, xn-1,. . . , xi, . . . , x1 is descending at this moment.
If yi ≥ xi then there exists yi = kxi+r, where k = ⌊yi/xi⌋ and 0 ≤ r < xi, namely r = MOD(yi, xi) < xi. We obtain:
| (34) |
Apparently yi-k < xi-k, xi-(k+1) = yi-k < xi-k. Therefore the chain xn, xn-1, . . . , xi, . . . , x1 is always descending. Because xi ∈ N(i = n, n - 1, . . .), there must exist x1 = 0 and the program will terminate.
Assume the induction hypothesis that the relation formula between input variables xn-1 and yn-1 and output value z namely rn-1xn-1 + sn-1yn-1 - z =rn-1xn-1 + sn-1yn-1 - y1 = 0 is true, namely output variable value z = GCD(xn-1, yn-1) = rn-1xn-1 +sn-1yn-1 = y1. We need to prove that there exists F = rnxn+snyn-y1 = 0, namely z = GCD(xn, yn) =rnxn + snyn= y1.
| (35) |
If yn < xn, we use F to be divided by f*1 and f*2 to obtain:
| (36) |
Let, R = snxn-1 + rnyn-1 - y1 = 0, we obtain Wu’s characteristic set {f*1, f*2, R} and
where, In(f*1) = 1 and In(f*2) =1. When sn = rn-1, rn = sn-1, P = F = 0. Obviously output variable value z = GCD(xn, yn) = rnxn + snyn = y1.
If yn≥xn, we use F to be divided by f*3 and f*4 to obtain:
| (37) |
Let, R = (rn + sn)xn-1 + snyn-1 - y1, we obtain Wu’s characteristic set {f*3, f*4, R} and
where, In(f*3) = 1 and In(f*4) =1. When rn = rn-1 - sn-1, sn = sn-1, P = F = 0. Here we can prove that output variable value z = GCD(xn, yn) = rnxn + snyn = y1.
Therefore, there exists rn ∈ Z and sn ∈ Z and the relation formula between input variables xn and yn and output variable value z namely F = rnxn +snyn -z = rnxn + snyn - y1 = 0 and output value z = GCD(xn, yn) =GCD (x*, y*) = y1. The program is partially correct. Because termination has been proved, we can obtain the program is totally correct.
| Fig. 1: | The result of proving the program GCD |
We conducted our project in our lab and completed the necessary experiments from Sep 2009 to Nov 2009. We make program to implement our reasoning to prove the total correctness of the example on automated reasoning platform MMP (http://www.mmrc.iss.ac.cn/mmp). We give variables’ ordering and extract state transition equations, terminate condition and goal and transform them into algebraic formulae and triangularize state transition equations. The formulae are the input of our program and the program can automatically generate invariants and compute to decide whether the recursive program is partially correct and will terminate. The result is shown in Fig. 1.
SIf the program does not terminate, we can prove that it dose not satisfy termination condition. The example (Example 2) is shown as follow:
| (38) |
First, we extract termination condition, state transition equations and goal from the program and triangularize constraint conditions.
Termination condition:
| (39) |
State transition equations (constraint conditions):
| (40) |
| (41) |
Goal:
| (42) |
But the Example 2 may not terminate. When the relation formula among program states is reduced with respect to state transition equations, the corresponding states do not satisfy termination condition.
Proof: It can be easily seen that xn, xn - 1, . . ., xi, . . ., x1 form a descending chain and there may exist xm = 0 if ym > 0. For the sake of simplicity let m = 1.
| Fig. 2: | The result of proving the program GCD1 |
According to relation formula among the states and state transition equations, if x1 = 0 and y1 > 0, then y1 - z = 0 and x1 = 0 which satisfies termination condition. We obtain the program will terminate and output value z = y1 at this moment.
Similarly yn, yn-1, . . ., yi, . . ., y1 form a descending chain and there may exist ym = 0 if xm > 0. Let m = 1 and if y1 = 0 and x1 > 0, then F = x1-z = 0 is reduced with respect to f*1 = x1-y1-x0 = 0 and f*2 =y1 - y0 = 0 and y1 = 0 does not satisfy termination condition. Because x1 > y1, we should apply f*1, f*2 to pseudo-division to obtain R1. Wu’s characteristic set {f*1, f*2 R1} is obtained, but after computation we know R1 = x1 - z = F and F is reduced with respect to f*1, and f*2. Because x1 > y1 again, f*1 and f*2 will be applied to pseudo-division to obtain R1 repeatedly and the process will be infinite. The program will not terminate when y1 = 0.
The result of proving program GCD1 on a PC with automated reasoning platform MMP is as shown in Fig. 2.
Definition 7: The states of program are reduced if the corresponding relation formula among the program states is reduced with respect to state transition equations.
From above discussion we know that if the reduced states of program do not satisfy termination condition, then the program will not terminate.
Suppose that the program will terminate, there must exist states satisfy termination condition and the reduced states will be transformed into termination states. Let, f be the corresponding relation formula among the reduced states. According to definition 7 and theorem 1 we use f to be divided by state transition equations to obtain pseudo-remainder R = f. The reduced states do not change in pseudo-remainder R and will not be transformed into termination states forever (there exits a infinite sequence of reduced states). This yields a contradiction. Therefore the program will not terminate.
EXPERIMENTS
The theorem prover Isabelle (http://www.isabelle.in.tum.de/) is a generic system for implementing logical formalisms and Isabelle/HOL is the specialization of Isabelle for HOL (high order logic). As mentioned ealier, our method has been implemented on MMP in some examples. Similarly we use Isabelle to prove the correctness of the examples. Compared with the other traditional approaches such as Isabelle, our method is proved to be more efficient through experiments especially in polynomial program. Its performance can be seen in Table 1. The experimental environment was an Intel Pentium 4 with 1.8 GHz of processor and 512 MB of memory.
We use Isabelle2008 to prove the examples on windows platform through simulator Cygwin which simulates a Unix-like environment. We generate some definitions, funs and lemmas etc for proving the examples.
| Table 1: | The comparison of execution time of experiment results between Isabelle and MMP (in sec) |
Factorial: 1 primrec and 5 lemmas; Fibonacci: 1 definition and 12 lemmas; Gauss: 1 primrec and 7 lemmas; GCD: 3 definitions, 1 fun and 20 lemmas.
CONCLUSIONS
There exists quite a lot formal verification approaches to prove program correctness. If we can make program correctness proving algebraized, the efficiency of proving will be improved greatly and it will be mechanized and automated easily. In this study, we transform program into algebraic transition system and apply Wu’s method to recursive program correctness proving. The new approach gives new theoretical insights into program correctness proving. Compared classical formal method, our method is more efficient in many programs especially in polynomial program; compared (Popov and Jebelean (2009) our method more widely applicable because the method by Popov and Jebelean (2009) can only be applicable to Tail Recursive Programs which have a specific structure and dose not include multi-ply conditional statement etc. Mathematics mechanization is a powerful and promising methodology in program correctness proving. There exists diversiform programs and their proving methods should be diversiform. We need combine diversified program verification techniques to settle complicated verification problems.
ACKNOWLEDGMENTS
The results described in this study was supported by a grant from the National Science Foundation of China (NSFC) (60671033) and the Doctoral Foundation of the Ministry of Education of China (2006061405).