On the termination of simple computer programs

Abstract

In the area of semantics of programming languages the problem of calculating the termination domain (the set of inputs for which a program terminates) is considered: For simple non-nested loop-programs compile-time testable conditions are given such that the resp. programs are total (terminate for all inputs). Auxiliary tool is a global (=mathematical) semantics for infinite loop-programs whose properties are studied in detail. An application yields a proof that the well-known termination proof technique of Floyd cannot be generalized, i.e. you only have to look for statements of the form y:=y+k and a suitable condition controlling the loop and not for more complicated ones.

This paper is an overview on a part of the author's doct. dissertation.