A Hoare-like verification system for a language with an exception handling mechanism

AbstractThis paper presents a Hoare-like system for the language Lexc containing typical statements, recursive procedures and an exception handling mechanism. The exception handling mechanism supports both termination and resumption as handler responses to an exception The semantics of the language is defined by a copy rule. The Hoare-like system is based on the system defined in Olderog (1981) for an Algol-like language. It is relatively complete for programs with a finite C-index (C stands for a copy rule). The example of a correctness proof fo a simple program is presented