Two New Strategies for Developing Loop Invariants and Their Applications

The loop invariants take a very important role in the design,proof and derivation of the algorithmic program.We point out the limitations of the traditional standard strategy for developing loop invariants, and propose two new strategies for proving the existing algorithmic program and developing new ones. The strategies use recurrence as vehicle and integrate some effective methods of designing algorithms, e.g.Dynamic Programming,Greedy and Divide Conquer,into the recurrence relation of problem solving sequence.This lets us get straightforward an approach for solving a variety of complicated prob- lems,and makes the standard proof and formal derivation of their algorithmic programs possible.We show the method and advantages of applying the strategies with several typical nontrivial examples.

Nonlinear Program Construction and Verification Method Based on Partition Recursion and Morgan's Refinement Rules

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.

A Unified Approach for Developing EfficientAlgorithmic Programs

A unified approach called partition-and-recur for developing efficient and correct algorithmic programs is presented. An algorithm (represented by recurrence and initiation) is separated from program, and special attention is paid to algorithm manipulation rather than program calculus. An algorithm is exactly a set of mathematical formulae. It is easier for formal derivation and proof. After getting efficient and correct algorithm, a trivial transformation is used to get a final program. The approach covers several known algorithm design techniques, e.g. dynamic programming, greedy, divide-and-conquer and enumeration, etc. The techniques of partition and recurrence are not new. Partition is a general approach for dealing with complicated objects and is typically used in divide-and-conquer approach. Recurrence is used in algorithm analysis, in developing loop invariants and dynamic programming approach. The main contribution is combining two techniques used in typical algorithm development into a unified and systematic approach to develop general efficient algorithmic programs and presenting a new representation of algorithm that is easier for understanding and demonstrating the correctness and ingenuity of algorithmic programs.

A Shape Graph Logic and A Shape System

Analysis and verification of pointer programs are still difficult problems so far. This paper uses a shape graph logic and a shape system to solve these problems in two stages. First, shape graphs at every program point are constructed using an analysis tool. Then, they are used to support the verification of other properties （e.g., orderedness）. Our prototype supports automatic verification of programs manipulating complex data structures such as splay trees, treaps, AVL trees and AA trees, etc. The proposed shape graph logic, as an extension to Hoare logic, uses shape graphs directly as assertions. It can be used in the analysis and verification of programs manipulating mutable data structures. The benefit using shape graphs as assertions is that it is convenient for acquiring the relations between pointers in the verification stage. The proposed shape system requires programmers to provide lightweight shape declarations in recursive structure type declarations. It can help rule out programs that construct shapes deviating from what programmers expect （reflected in shape declarations） in the analysis stage. As a benefit, programmers need not provide specifications （e.g., pre-/post-conditions, loop invariants） about pointers. Moreover, we present a method doing verification in the second stage using traditional Hoare logic rules directly by eliminating aliasing with the aid of shape graphs. Thus, verification conditions could be discharged by general theorem provers.

A QUANTIFIER-ELIMINATION BASED HEURISTIC FOR AUTOMATICALLY GENERATING INDUCTIVE ASSERTIONS FOR PROGRAMS

A method using quantifier-elimination is proposed for automatically generating program invariants/inductive assertions. Given a program, inductive assertions, hypothesized as parameterized formulas in a theory, are associated with program locations. Parameters in inductive assertions are discovered by generating constraints on parameters by ensuring that an inductive assertion is indeed preserved by all execution paths leading to the associated location of the program. The method can be used to discover loop invariants-properties of variables that remain invariant at the entry of a loop. The parameterized formula can be successively refined by considering execution paths one by one; heuristics can be developed for determining the order in which the paths are considered. Initialization of program variables as well as the precondition and postcondition, if available, can also be used to further refine the hypothesized invariant. The method does not depend on the availability of the precondition and postcondition of a program. Constraints on parameters generated in this way are solved for possible values of parameters. If no solution is possible, this means that an invariant of the hypothesized form is not likely to exist for the loop under the assumptions/approximations made to generate the associated verification condition. Otherwise, if the parametric constraints are solvable, then under certain conditions on methods for generating these constraints, the strongest possible invariant of the hypothesized form can be generated from most general solutions of the parametric constraints. The approach is illustrated using the logical languages of conjunction of polynomial equations as well as Presburger arithmetic for expressing assertions.

A Unified Strategy for Formal Derivation and Proof of Binary Tree Nonrecursive Algorithms

In the formal derivation and proof of binary tree algorithms,Dijkstra’s weakest predicate method is commonly used.However,the method has some drawbacks,including a time-consuming derivation process,complicated loop invariants,and the inability to generate executable programs from the specification.This paper proposes a unified strategy for the formal derivation and proof of binary tree non-recursive algorithms to address these issues.First,binary tree problem solving sequences are decomposed into two types of recursive relations based on queue and stack,and two corresponding loop invariant templates are constructed.Second,high-reliability Apla(abstract programming language)programs are derived using recursive relations and loop invariants.Finally,Apla programs are converted automatically into C++executable programs.Two types of problems with binary tree queue and stack recursive relations are used as examples,and their formal derivation and proof are performed to validate the proposed strategy’s effectiveness.This strategy improves the efficiency and correctness of binary tree algorithm derivation.

A Method to Deduce and Synthesize the Dafny Programs

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.