The Weakest Pre-Predicate Generator Design And Implementation Based PAR

Starting from the sixties of last century, with the rapid development of large-scale software, people higher up the software quality requirements, especially for the correctness of the software requirements。Computer industry to ensure the software quality, especially high-reliability software made many new theoretical research, is one proof of program, Proof of program is the rigorous mathematical method to evaluate whether a program meets a given performance。Program verification officers take some time and effort to master the knowledge of the correct procedure because the process that needs to involve a large number of mathematical symbols and mathematical theories of knowledge makes。And even as it relates to verify the mathematical theory of a short procedure also requires the verification process more cumbersome, often resulting proof procedures than to prove a lot more complex situation,These unfavorable conditions in which the program correctness relying solely on manual verification to prove that if there could be many adverse consequences.。For example, inefficient verification, validation and so the resulting data unreliable。To overcome the manual verification process of the correct procedures for adverse effects caused by many computer scientists began to use machines to automatic verification process to gradually reduce the human intervention program verification process, the ultimate aim is to verify the correctness of the procedure to move toward full automation。According to Dijkstra's weakest pre-predicate theory, if we can prove Q ==> WP("S",R);Were able to determine the correct procedure,Based on this theory,as an integral part of the PAR platform goal is to develop an Apla program automatically calculates the weakest front-predicate system, reducing manual intervention Apla program verification,The known S, R to automatically solve the weakest pre-predicate.。1,Deep understanding of the Dijkstra weakest in front based on the predicate of the language automatically calculate the weakest pre-predicate APLA algorithm。2,Select a number of Apla test procedures, test results show that the system has implemented automatically calculate the weakest pre-predicate function。3,Dijkstra weakest attempt to automatically generates pre-predicate device platform, integrated into the PAR, PAR to become an auxiliary tool; can effectively support the PAR platform。Further work includes a comprehensive system conversion mechanism; improve system reliability; Enhance the complexity of the algorithm and the classical algorithm for digital analysis and solution of the problem。...