Verification of programs with procedure-type parameters Article

Ernst, GW, Navlakha, JK, Ogden, WF. (1982). Verification of programs with procedure-type parameters . Acta Informatica, 18(2), 149-169. 10.1007/BF00264436

cited authors

  • Ernst, GW; Navlakha, JK; Ogden, WF

abstract

  • A verification system is developed for proving the correctness of programs containing procedures with procedure-type parameters. The system, which reduces programs and their specifications to assertions to be proved in ordinary logic, is shown to be logically sound. The reduction process is controlled by the syntax of the program and is completely mechanical, requiring no human intervention. The resulting assertions involve higher-order predicates, but they engender no significant difficulties which are not already present in ordinary first-order theories. Our system views the intermediate objects in the reduction process as extended programs, thereby making verification a much less abstruse process. Treating logical assertions as commands appeals strongly to a programmer's intuition. © 1982 Springer-Verlag.

authors

publication date

  • November 1, 1982

published in

Digital Object Identifier (DOI)

start page

  • 149

end page

  • 169

volume

  • 18

issue

  • 2