The Research Of Software Formal Verification Technology Based On Hoare Logic

Today, most software is of large scale, so the programmers have paid more attention to their safety. But until now, the safety guarantee provided by existing programming language and software engineering technology is weak and unreliable. For instance, in the production of software, standard engineering method and intensive testing are used to decrease bugs. However, it can't be guaranteed that there are no bugs after intensive testing, and these methods are not strictly repeatable processes. It can be asserted that existing software engineering techniques can't improve the software safety and security essentially, but, program verification based on Hoare Logic can provide guarantee for software safety.Considering that current methods of verification are not repeatable, this dissertation proposes a formal and repeatable method of paraphrasing code into its semantics, and addresses the issue of repeatability and practicality in program verification activities based on the strongest postcondition predicate transformer of Hoare Logic.First of all, we discuss the theoretical problems with automating existing strongest postcondition calculations for assignment. We provide a definition for sp to calculate the strongest postcondition for assignment, which can be mechanized and which does not rely on the calculation of inverse functions or on the introduction of new variables.Secondly, considering that the depth of loop must be known before calculating the loop semantics, this paper introduces an approach to the analysis of loop progress and termination conditions in imperative programs. The approach involves the algorithmic derivation of loop progress and termination conditions directly from the code itself. We can use the loop semantic information generated by the method to support program verification and defect correction.Once again, existing method for calculating the strongest postcondition for a procedure call is hindered because the strongest postcondition for the procedure body must be calculated every time it is called. Considering this deficiency, we present algorithms for using the strongest postcondition for deriving specifications directly from code for procedures and for deriving specifications of the semantic effects of calling those procedures.Finally, we have described verification methods based on the derived semantic forms in the last of the thesis. Three methods of formal verification have been presented. The contribution is that it provides a strategy for using the information generated by the algorithms and techniques above for supporting both semi-formal and formal verification.