Termination assertions for recursive programs: Completeness and axiomatic definability

  • Meyer A
  • Mitchell J
  • 1

    Readers

    Mendeley users who have this article in their library.
  • 5

    Citations

    Citations of this article.

Abstract

The termination assertion p〈S〉 q means that whenever the formula p is true, there is an execution of the possibly nondeterministic program S which terminates in a state in which q is true. The program S may declare and use local variables and nondeterministic procedures with call-by-value and call-by-address parameters. In addition, the program may call undeclared global procedures. Formulas p and q are first-order formulas extended to express hypotheses about the termination of calls to undeclared procedures. A complete effective axiom system with rules corresponding to the syntax of the programming language is given for the termination assertions valid over all interpretations. Termination assertions define the semantics of programs in the following sense: if two programs have different input-output semantics, then there is a temination assertion that is valid for one program but not the other. Thus the complete axiomatization of termination assertions is an axiomatic definition of the semantics of recursive programs. © 1983 Academic Press, Inc.

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document

Authors

  • Albert R. Meyer

  • John C. Mitchell

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free