A general theorem on the total correctness of programs in a category

AbstractIn [7], we presented a completeness theorem for proving partial correctness of programs in a large class of categories. This theorem generalized a classical result of S.Cook [5] for the language of while-programs.Here we address the total correctness of programs. Again, we use the semantics based on partially additive categories, which was introduced by M.A.Arbib and E.G.Manes [3,4,6]. Our theorems generalize the non categorical results of K.R.Apt [1,2]. They are valid for a large class of partially additive categories, including the category of sets and partial functions and the category of sets and relations, i.e. for deterministic and nondeterministic programs