A Research Of Software Correctness Analysis Based On Weakest Precondition

With the constant iteration of software,the necessity of software correctness detection is increasing,and the processing time of software correctness detection directly determines the maintenance cost of the software.Although the assertion of dynamic test and the symbolic execution of static analysis are optimized for software correctness,the analysis results are still prone to problems such as missing paths or even unrecognized errors,etc.Furthermore,the existing verification methods are easy to generate many useless paths or incur insufficient targeting when the paths are extended.Hence,it is very crucial to study a more reliable solution.This paper proposes a semi-automatic software test system based on the weakest precondition(SAST)which applies static analysis techniques and White-Box Testing technique and analyzes the program correctness based on the weakest precondition.A program is a key part of a software because the program correctness is a prerequisite for an entire software correctness.Considering current practical issues,the system researches as follows:1.The system mainly studies three kinds of program structure statements,which to be specific,using program slicing technology to preprocess the program codes of assignment statement,selective structure statement and loop structure statement.Then use symbolic execution to process the preconditions and post conditions.And it describes the derivation process and path extension methods of three kinds of program structure.Finally,the system expands coverage of test codes,adding nesting of for-loop structure and switch selective structure statement.2.The system adds statistical function of program execution time and the function of hierarchical relationship between codes,which can optimize the module quality of codes,and reduce the effective time of path analysis and the cost of software testing.In addition,the system has a user interaction window which is convenient for users to input data and display results.3.The system can effectively reduce the loss of verification accuracy incurred by static analysis on the program state abstraction operations and figure out all possible paths of the program.Then group and mark the true and false values of the condition expressions to verify the path correctness.While analyze the correctness of highly complex program codes efficiently.