Proof rules for gotos |
| |
| Authors: | Michael A Arbib Suad Alagić |
| |
| Affiliation: | (1) Department of Computer and Information Science, University of Massachusetts, 01003 Amherst, MA, USA;(2) Department of Informatics, Electrotechnical Faculty, University of Sarajevo, 71000 Sarajevo-Lukavica, Yugoslavia |
| |
| Abstract: | Summary We offer a program specification format adapted to statements with multiple exits, and use it to present proof rules to replace the somewhat unsatisfactory treatment of jumps in 3]. We justify the  bridled use of gotos in return exits, failure exits, and loops with jumps in the middle. To exemplify our methodology, we prove the function Lookup. |
| |
| Keywords: | |
| 本文献已被 SpringerLink 等数据库收录！ |
|
