Verification Of Program Correctness Based On Tense Logic

At present the development of computer software is being affected by a variety of factors, which lags behind the hardware, its safety, reliability and stability has been a concern of several important issues. With the large-scale, systematic, and security requirements of software increase, people higher up the software quality requirements, especially for the correctness of the software requirements. Software long-standing quality problem, due to run in a number of key areas of software quality problems caused major losses or even catastrophe, are not uncommon.Methods based on debugging have many limitations. There still are hidden errors in the system program or application after debugging and running. Therefore, in order to ensure the program is correct, it is necessary to study the process in theory to prove the correctness. Computer scientists prove the consistency of programs with the function of reduction to ensure the program is correct in a fully formal way. Formal verification of the completely correctness is formulated as partial correctness and termination by formal proof method.The option to solve the issue as a breakthrough, proposed a new automatic verification method based on formal theory for direction: namely, proof of program correctness based on tense logic. Tense logic is based on the first-order logic through the introduction of time variable explicitly obtained by a logical. This logic is used to describe the semantics of the various language components, the property of the verification process, and software specifications of programming language. Compiler technology using a combination of compiler for C language type definitions, variable definitions, operators, expressions, statements, function definitions and semantics of function call will be translated into temporal logic formulas. Finally the resolution principle that procedural in property and norms must meet their needs analysis and design phases to achieve goals.ANSI C program as input object, a detailed description of the compiler lexical analysis, syntax analysis generated by BISON, semantic analysis, syntax tree generation, are given. It provides the principles and algorithms which are extended to the resolution principle of tense logic.