On the total correctness of nondeterministic programs

For an arbitrary programming language with nondeterminism to be implementable, the existence of computation trees modelling the possible changes in state in the course of a computation is postulated. A general definition of what constitutes an execution method is then presented. Falling naturally out of these ideas is the correspondence between execution methods and total correctness, in that different properties are required of a program to be correct when different methods are adopted. We describe a variety of plausible methods of execution falling under the general definition and single out four particular ones. The arguments made are then illustrated by analysing the properties required by Dijkstra of guarded commands in view of these four methods. We conclude that a general approach such as that suggested here seems to be needed for dealing with programming languages and execution methods other than the particular ones treated by Dijkstra.     

Proving total correctness of nondeterministic programs in infinitary logic

Summary It is shown how the weakest precondition approach to proving total correctness of nondeterministic programs can be formalized in infinitary logic. The weakest precondition technique is extended to hierarchically structured programs by adding a new primitive statement for operational abstraction, the nondeterministic assignment statement, to the guarded commands of Dijkstra. The infinitary logic L ₁ is shown to be strong enough to express the weakest preconditions for Dijkstra's guarded commands, but too weak for the extended guarded commands. Two possible solutions are considered: going to the essentially stronger infinitary logic L ₁₁ and restricting the power of the nondeterministic assignment statement in a way which allows the weakest preconditions to be expressed in L ₁.     

Total correctness of CSP programs

Summary In this paper we propose an axiomatic system for proving the total correctness of CSP programs. The system is based on the partial correctness system of [6, 7]. We use the proposed system to prove the total correctness of a program for set partitioning.This work was supported in part by the NSF grant no. ECS8404725     

Axiomatic approach to computational attention

Here we describe, in terms of a decision problem, any situation in which a computational system will be forced to allocate attention at any time to one spatial location to improve the reconstruction fidelity on a neighborhood of the chosen point. The result is a rational model of computational attention in which a multi-bitrate attention map will provide us with the attention score for each spatial location at high and low quality versions of the image reconstruction. At any time a rational system should choose, even though without any outside knowledge, among alternative spatial locations in such a way as to avoid certain forms of behavioral inconsistency. We compare the performance between a rational approach of computational attention and various models for predicting visual target distinctness, using scenes that represent military vehicles in complex rural backgrounds.     

Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods

We present a symbolic-numeric hybrid method, based on sum-of-squares （SOS） relaxation and rational vec- tor recovery, to compute inequality invariants and ranking functions for proving total correctness and generating pre- conditions for programs. The SOS relaxation method is used to compute approximate invariants and approximate rank- ing functions with floating point coefficients. Then Gauss- Newton refinement and rational vector recovery are applied to approximate polynomials to obtain candidate polynomials with rational coefficients, which exactly satisfy the conditions of invariants and ranking functions. In the end, several exam- ples are given to show the effectiveness of our method.     

Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods

We present a symbolic-numeric hybrid method, based on sum-of-squares (SOS) relaxation and rational vector recovery, to compute inequality invariants and ranking functions for proving total correctness and generating preconditions for programs. The SOS relaxation method is used to compute approximate invariants and approximate ranking functions with floating point coefficients. Then Gauss-Newton refinement and rational vector recovery are applied to approximate polynomials to obtain candidate polynomials with rational coefficients, which exactly satisfy the conditions of invariants and ranking functions. In the end, several examples are given to show the effectiveness of our method.     

Estimating the correctness of computer programs

Program testing will for some time remain the major means by which program designers convince themselves and others of the correctness or validity of their programs. Thus it is desirable to be able to use test results to measure the degree to which a program approaches correctness. The probability of correctness of a program can sometimes be estimated according to the success of testing. A general parameter is introduced which has the property that its value is zero for a correct program and is greater than zero for an incorrect program. Under reasonable interpretations, the parameter is related, through probability density functions, to characteristics which are observable through program testing. For instance, if the parameter is interpreted as the number of errors in a program, a related, observable characteristic is the number of errors discovered through testing. Upper bounds on the parameter value are established as a function of the value of the observed characteristic and the desired level of confidence in the result. Results are presented for cases of combinations of interpretations, observable characteristics, and probability density functions.     

Axioms for total correctness

Summary A notation for total correctness of a program with respect to input and output formulas is introduced; and Hoare's loop axiom is rearranged in such a way as to form a good inference system for the total correctness. Its consistency and completeness are shown.     

General correctness: A unification of partial and total correctness

Summary General correctness, which subsumes partial and total correctness, is defined for both weakest preconditions and strongest postconditions. Healthiness properties for general-correctness predicate transformers are more uniform and complete than those for partial- and total-correctness systems. In fact, the healthiness properties for partial and total correctness are simple restrictions of those for general correctness. General correctness allows simple formulations of the connections between weakest and strongest postconditions and between the notions of weakest precondition under the demonic and angelic interpretations of nondeterminism. A problem that plagues sp-sp(P, C) is undefined if execution of C begun in some state of P may not terminate — disappears with the generalization.This paper is a study of some simple theory underlying predicate transformer semantics, and as yet has little bearing on current programming practices. The theory uses a relational model of programs.This work was supported by the National Science Foundation under grant MCS-81-03605 and by the second author's Guggenheim Fellowship. This paper is based on the first author's Ph.D. thesis at Cornell.     

Generation of correctness conditions for imperative programs

Verification of imperative programs in the sense of Floyd-Hoare is an approach to proving correctness of programs annotated by preconditions, postconditions, and loop invariants. It is based on generation of correctness conditions. In the structured deterministic case, the problem of generation of correctness conditions seems trivial, since it is solved by a syntax-driven algorithm, the complexity of which linearly depends on the number of control constructs. Vice versa, in the unstructured nondeterministic case, it seems a priori clear that the complexity of generation of the correctness conditions exponentially depends on the number of statements in the program. In the paper, an efficient and complete algorithm for the generation of the correctness conditions is presented and justified. It can be used both in the structured deterministic and unstructured nondeterministic cases. The algorithm complexity linearly depends on the number of control constructs and/or program statements.     

Total correctness in nonstandard logics of programs

We show that termination is a first-order notion if approached via Nonstandard Logics of Programs (NLP). We give explicit first-order characterizations of the program-verifying power of the well-known Manna-Cooper method for proving total correctness assertions (tca's). Similar characterization is given to the Intermittent Assertions Method (w.r.t. tca's). A comparison of the tca-proving powers of distinguished methods (or logics of programs) is also attempted. We also show that NLP provides new methods which are strictly stronger than the Manna-Cooper method. In the end we turn to partial correctness issues related to the main body of the paper.     

A structured approach to static semantics correctness

An approach to the correctness proof of static semantics with respect to the standard semantics of a programming language is presented, where correctness means that the properties of the language described by the static semantics, such as type checking, are consistent with the standard semantics. The standard and static semantics are given in a denotational style in terms of some basic domains and domain constructors, which, together with suitable operations, are used to describe fundamental semantic concepts. The domains have different meaning in the two semantics and the static semantics correctness proof is carried out by devising a set of suitable functions between them. We show that the correctness proof can be greatly simplified by structuring the semantics definitions, and we illustrate that by applying the methodology to a simple imperative language. In the example the derivation of a static checking algorithm from the static semantics is described.     

An elementary and unified approach to program correctness

We present through the algorithmic language DHL (Dijkstra-Hehner language), a practical approach to a simple first order theory based on calculational logic, unifying Hoare and Dijkstra’s iterative style of programming with Hehner’s recursive predicative programming theory, getting the “best of the two worlds” and without having to recur in any way to higher-order approaches such as predicate transformers, Hoare logic, fixed-point or relational theory.