A program verification system
| Autor: | George W. Ernst, Raymond J. Hookway |
|---|---|
| Rok vydání: | 1976 |
| Předmět: |
Bubble sort
Theoretical computer science Computer science Programming language Verification system Pascal (programming language) Solver Verification condition generator computer.software_genre Intelligent verification Automated theorem proving TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Program analysis TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS computer computer.programming_language |
| Zdroj: | ACM Annual Conference |
| DOI: | 10.1145/800191.805651 |
| Popis: | A program verification system has been developed consisting of three major components. The verification condition generator(which is patterned after the work of Igarashi, London, and Luckham [10]) is used to generate verification conditions from asserted PASCAL programs. The subgoal generator(which is similar to the program described in [2])processes the verification conditions to produce simpler subgoals, a significant number of which it proves using restricted techniques. The subgoal solveris a resolution theorem prover which was developed at NIH by L. Norton [13]. The more powerful techniques of the subgoal solver are used to prove subgoals which the subgoal generator was unable to prove.The verification system has been used to verify a number of programs. These include all but one of the examples from King [11], a Bubble Sort program, and Hoare's FIND program. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|