Can we quantify how close a partially correct programs is to being correct?

Question

I know that there is something called partial correctness, but I was wondering if there was a way to tell how close a semi-correct program is to a fully correct program.

For example, if you had a sorting program that almost completely sorts an array, could you use Hoare logic to determine how close it is to getting the correct answer? One way to do this would be to make the precondition a series of and statements and see how many of these statements the weakest precondition, resulting from the postcondition being propagated through the program, would be able to imply.

However, this method seems to be very crude. Is there any other way to do something like this?

Answer 1

Partial correctness does not mean that not all statements of a specification are met by an algorithm. Have a look at the Wikipedia article about correctness:

Partial correctness of an algorithm means that it returns the correct answer if it terminates.

Total correctness means that is it additionally guaranteed that the algorithm terminates.

Such a proof of termination can e.g. be done by a loop variant: To proof that a loop terminates we show that an integer expression is decreased in the loop body and that the expression stays always non-negative. Then the loop can be only iterated a finite number of times. The B-Method uses such integer variants in its while loops. An alternative for an integer expression would be a finite set where in each iteration an element is removed.

Example: A simple algorithm to initialise an array of size n with 0:

i := 0
while i<n do
  x[i] := 0
  i := i+1
done

Partial correctness can be proven by using a loop invariant ("all elements of x in 0..i are 0", 0<=i, i<=n). One must show that the invariant is fulfilled when entering the loop and after each iteration. After the loop we know that the invariant is fulfilled and the loop condition not (i>=n together with the loop invariant implies that i=n, that again implies "all elements of x in 0..n are 0"). Even if we forget the line i := i+1, we could prove the partial correctness of the algorithm, i.e. the array will be filled with 0 after termination. The problem would be that it does not terminate.

Termination can be shown by choosing n-i as a variant. With the invariant i<=n it can be proven that the variant is always non-negative and n-i is decreased (by increasing i) in every iteration. Thus the loop must terminate. Together with partial correctness, total correctness is shown.

Answer 2

In a nutshell:

Partial correctness is an issue of termination, not ot correctness of what is computed. A function is partially correct with respect to a specification iff whatever it computes is correct, when it terminates. This idea can be extended to the computation of incomplete (partial) answers. Whatever is computed of the answer is correct, but the program may at some point go into a non-terminating loop, possibly without having computed all of the answer. Partial answers are approximations of complete answers.

This approximation structure is a partial order, which is the basic concept of Scott's semantics domains,and it can actually be used to answer another interpretation of the question. Can we measure a distance between a correct answer and a not quite correct one, such as having one element of an array that is wrong (rather than unknown). One way to define such a distance is to consider the approximation ordering, and relate the two incompatible answers (the correct one and the incorrect one) to the best partial answer that is an approximation of both. This issue is quickly looked at from the point of view of numerical analysis, where precision analysis is essential, and of some other areas.

This second point is actually explored in a second answer to the question, as I did not realize at first that the two answers could have a connection. But both answers are quite long, and I did not feel wise to merge them when I realized the connection.

A first simple view of partial correctness

There is no such thing as being (partially) correct in an absolute sense. A program is correct if it meets a specification, however given. The specification may be another program, or a logical statement, or whatever can be formalized. The specification must somehow include information on when the program terminates, possibly always (which is actually assumed in most definitions, so that nothing more complex needs to be said). Actually the domain may be restricted in the specification to the part where termination is expected, so that termination is always expected, which may justify assuming termination in the whole domain in the usual definition (wikipedia and wikipedia). This in turn imposes an implicit assumption on any specification, which may be, or may not be, so convenient.

A program $P$ is correct with respect to a specification $S$ iff it terminates whenever the specification says it should, and with a result that meets the specification. It is partially correct iff it sometimes does not terminate where the specification says it should, but always gives a correct result when terminating.

As a consequence, a program that never terminates is partially correct with respect to any specification.

I chose a slightly extended definition also because it corresponds precisely to the notion of approximation in Scott's semantic domains, such as used in denotational semantics. A Scott domain includes a partial order corresponding precisely to th the idea of partial correctness (the two uses of the word "partial" are somewhat unrelated). A function $F$ is and approximation of a function $G$ is $G$ terminates whenever $F$ terminates, and both give then the same result. So $G$ may give a result when $F$ does not. And we can say that $F$ is partially correct with respect to $G$, or that $F$ approximate $G$, or $F\sqsubseteq G$.

These ideas are essential to define the semantics of functions with loop (or recursion) as the limit of an infinite set of functions without loop or recursion. See for example wikipedia, or a very informal presentation on SE.

Standard Hoare logic will work only to prove partial correctness, and need to be extended to address termination properties, hence to address total correctness (see wikipedia). There are implemented examples of such specific extensions.

Proving total correctness amounts to proving partial correctness and termination. Hoare logic is quite appropriate for partial correctness. Proving termination requires usually a proof by induction (recurrence) which is the natural approach to proving things in Scott's semantics (as the semantics itself is defined that way, inductively). The answer by danielp shows how such an induction can complement a proof in Hoare's logic.

As to quantifying partial correctness, assuming you still want to do so, it could be by somehow identifying the parts of the domain where the program does or does not terminate, or some properties of those parts.

Extension to complex results, applied to the sorting example.

Actually, the issue can be a bit more complex, when you consider complex answers, such as data structures (which is the case when sorting arrays). The specification could require the computation of two answers (i.e., a pair), and for some parts of the input domain an actual program could find one element of the pair, but not terminate while computing the other, in other cases find only the other element, or find both, or find none. This is still approximation in Scott sense, and such a program is partially correct.

More generally, the idea of approximation in the Scott sense applies to data as well as to program. For that, informally, you need the concept of an unknown answer (not yet computed, possibly never known if its computation does not terminate). It is usually represented by the symbol $\perp$. The pair $(\perp,36)$ approximates $(25,36)$. What you get on a program that delivers the 36 part and then does not terminate can be represented by $(\perp,36)$.

How can this be applied to a program that sorts arrays of five integers? Suppose you write a program SORT5 that runs in parallel to your main application (I am trying to make things realistic), and is supposed to sort such an array for the application. The program SORT5 is supposed to store its result in some array provided by the application, and it can do so separately for each element, as soon as it knows where to place it. It first looks for the largest and the smallest, and stores them at both ends, then it tries to do a recursion (or whatever), but has a bug that sends it into an infinite loop without any further results. The main application still gets a partial answer. If the array to be sorted was $[25, 36, 3, 9, 12]$, the answer provided is $[3,\perp,\perp,\perp,36]$ instead of $[3,9,12,25,36]$. Whatever is provided is correct, and the rest is not computed, so that you have only part of the answer. You thus have an approximation of the desired result. If you can prove that that is always the case, then your buggy program SORT5 that does not terminate is still partially correct with respect to the specification of a sort program.

A partially correct program can be useful. It could be that you did not really need sorting, but only the largest and smallest element. In that case the fact that your sort program SORT5 does not terminate and is only partially correct will not matter, and you application will work and hopefully terminate with a correct answer.

But who will stop your rogue sorting algorithm that will go on wasting computing power? There are computation strategies (lazy evaluation), that will not run a subprogram when more information on its result is not currently needed. So after you got the largest and smallest element, the program SORT5 would be on hold until other elements are asked for.

In this case, of course, there could be a way of quantifying the partial correctness. However I am not sure it would be very useful.

In this context, is necessary to revise a bit the definition, which I am doing somewhat informally:

A program P is partially correct with respect to a specification S iff it gives a complete answer that meets the specification before terminating, or provides part of an answer that meets the specification before going into a non terminating computation that provides no further part of the answer.

Then, a program that never terminates, and produces no part of result, is partially correct with respect to any specification.

Note that this definition leaves out a program that keeps computing, ever producing new parts of the answer. But since it does not produce infinitesimals (I do not know that this could make computational sense), it is actually computing an infinite answer.

These techniques can actually be very fruitful to formalize the semantics of computation of infinite object (only for very patient users), such as the exact decimal (or binary) representation of the value of $\pi$, or infinite lists. There are other interesting applications. But this is far from the initial question, and that is why I am leaving it out.

Answer 3

Quantifying the correctness of programs is actually a pretty hot topic in the context of formal methods, nowadays. Instead of posting a list of references, you may start here¹ (full version here) and continue from the references. Disclosure: this paper is a work of mine.

A brief summary of this work: we introduce a specification formalism that augments linear temporal logic by a set of "quality functions". These functions are chosen by the designer, thus giving the designer the ability to define quality as he pleases.

We show that model-checking for this logic is in PSPACE. Using the appropriate quality functions, you can measure e.g. the distance of an array from a sorted one.

---

1. Formalizing and reasoning about quality by S. Almagor, U. Boker and O. Kupferman (2013)

Answer 4

In principle it is possible to express this condition using something like Hoare logic, but it's not clear it will be very useful or practical to do so.

Consider a function $f$ in your program, with one argument. Suppose we have a predicate $P(x,y)$, expressing the condition that $y$ is the correct answer to the input $x$, i.e., if $f$ produces output $y$ on input $x$ then this output is correct. Also suppose we have a predicate $Q(y,y')$ expressing that the answers $y$ and $y'$ are close to each other. Define the predicate $R(x,y')$ by

$$R(x,y') \equiv \exists y . P(x,y) \land Q(y,y').$$

Then $R(x,y')$ expresses the condition you want, i.e., that $y'$ is close to the correct answer to the input $x$.

In your example, $P(x,y)$ could express the statement that $y$ is a sorted version of $x$, and $Q(y,y')$ could express some distance metric on lists (e.g., that $y'$ can be obtained from $y$ by a small number of transpositions).

Now that's just the problem of specification. There is a separate problem of verification, i.e., verifying that a function $f$ meets the spec $R$. The verification problem might be ugly and difficult in practice. And, verifying whether an implementation of a function meets a particular spec is undecidable in general, as jmite states. So, as always in verification, you're always dealing with undecidability (e.g., incompleteness).

Answer 5

Incorrectness

I wrote a first answer about partial correctness, which has a precise technical meaning. I thought better to separate this other answer which I initially though to be technically very different. It turns out not to be quite true, but both answers are long enough, so I thought better not to merge them

Apparently it seem that the OP is more interested in an idea of programs that are partly incorrect, of finding answers that incorrect in some respect, though, I guess, hopefully not too far of being correct.

There are actually two way you may want to consider closeness to correct for a function:

• whether computed answers have correct aand incorrect parts, or

• whether they are sometimes correct, and sometimes incorrect.

But these two aspects can be combined. If you manage to define something like a distance between values in the answer set, you can then try to extend that into a distance between functions that is, extremely informally, some kind of integral of the distance of their result for every point of their domain, or some other function of the incorrectness for every point of the domain.

Then the issue may be to determine if the distance between the completely correct function and the programmed one does not exceed some fixed threshold, or whether the error on the result of applying the function does not exceed for each domain point a threshold that may be related to this domain point.

These techniques may also be useful to do computation as correct as possible, with data that is in some sense not correct to begin with, such as experimental results. When the degree of incorrectness can be evaluated or hypothesized, this can help keep track of its effect on computation.

This is probably very dependent on the kind of data you are computing on.

I believe there is already such a theory for numerical computing, and is often applied for technical work, but I know little of it. Elementary aspects are often taught in physics courses.

Much numerical computation deals with real numbers. It cannot be exact (correct) because computer use only approximations of real numbers (there is a concept of computing with exact real arithmetics, but it is a very different topic, very much related theoretically to partial correctness). Aproximations in numerical computation cause small errors (rounding errors) that can propagate, and sometimes grow out of hand. Hence numericians have developed techniques to analyse their programs and evaluate how close the answer is to the correct result. They actually design their algorithms so as to minimize the computational errors, in addition to the other usual criteria, because the order of some operations may have a profound influence on the the size of the error being propagated.

These techniques are also important because they often have to deal with physical data that is itself only "close to correct", i.e. given with some approximation. Handling the errors on the input together with computational errors, and their propagation is, I believe, the object of significant research in the field of Numerical Analysis. But I am no expert. Some program will compute both the approximate result and an error interval around it where the correct answer is to be found. This compounds both the physical measurement errors and the numerical computation errors.

However, while this was essentially unavoidable in numerical mathematics dealing with reals (a continuous set of values), there no similar built-in limitation on symbolic computation, hence no obvious incentive, a priori, to develop similar techniques. Furthermore, it may not be obvious to do it.

Still, a close look at error handling techniques in parsing and natural language processing show that they actually use a similar conceptual view, even in a purely symbolic context.

The answer of Shaull seems to indicate that one may be interested in such approximation ideas in software engineering, but I am not sure it deals with the same concepts. I have not read his paper and I have read little of the litterature on this topic, and the answer gives no hint of the techniques he may be considering.

It may be a very different idea, since software engineering is much concerned with measuring how buggy the sofware may be, but inadvertantly buggy. I know that some statistical analyses show that various parameters that can be measured on a program are statistically related to the quality of the program, it maintainability and the likelihood of bugs.

The ides of approximate answers in numerical analysis (for example) is not a matter of bugs, but of handling the limitations of physical measurements, as well as the limitations of computing (which is inherently countable) when it is used to deal with reals (which are uncountable). If it is a bug, that is the fault of our universe, not of programmers.

Attempting to unify the issues: partial correctness and incorrectness measurement

The following is purely speculative, and an indication of work that could be done. I would suspect that at least some of it has been done already (I did not search thoroughly). But I do not recall reading about it and cannot give proper references. The description is only a sketch, and it is likely that much of it should be refined or made more precise, including the choice of definitions. I cannot garantee anything that I have not fully worked out mathematically (and even then ... :).

There is published litterature on real number computation based on definitions of real numbers approximations that organizes them in a Scott domain. Approximating reals with intervals is certainly a way to do it, and that is one proper way of developping a theory of computability over the reals. My guess is that it must have already been done, and it offers a good basis for a semantics theory, and for analysing real number crunching programs together with an assessment of the precision of the result as described above. (I did not have the opportunity to ask a specialist).

Now this may be a hint on what to do with symbolic computation, or with computation over the integers, to get a notion of approximately correct computation, espcially in the presence of complex data, i.e. the use of data structures.

The basic idea is the same as for real, use a concept of approximation and organize your computation domain (the values you compute with) as a Scoot domain. However, it will need to be something like a lattice, where two elements must have a greatest lower bound (glb or meet) as well as a least upper bound (lub or join). In the numerical case, the glb corresponds to the smallest interval containing 2 other intervals, and the lub to interval intersection.

Taking our sorting example from the first answer, sorting an array of 5 numbers $[25, 36, 3, 9, 12]$, we could consider all partial arrays as a lattice, and have:

• $lub([3,\perp,\perp,\perp,36], [\perp,9,\perp,\perp,36])=[3,9,\perp,\perp,36]$

• $glb([3,\perp,\perp,\perp,36], [7,9,\perp,\perp,36])=[\perp,\perp,\perp,\perp,36]$

Now, if you define a notion of distance in the order structure, then you can define the distance between two possible answers as the sum of their distances to their glb (or some other symmetrical and monotonically increasing function of these two distances).

If the domain does not have glb, you can take the distances according to each of the lower bounds (actually only the maximal elements of the set of lower bounds), and consider the smallest such distance (or possibly some other function of the distances of maximum elements, with adequate properties).

The inportant point is to have a tractable definition of correctness distance over the data you manipulate.

Then, this notion of distance can then be extended to mesuring distances between functions, which should be an answer to the question asked. I am not sure how much extra mathematical aparatus is needed, since some form of integration (in the calculus sense) may be needed.

A cursory search of the web about these issues yielded the following paper: "Towards Computing Distances between Programs via Scott Domains" which is already 15 years old. It should provide a better mathematical background. But I found it after writing this answer.

This problem can possibly be adressed with other logic, but I suspect it is much more an issue for the concept of approximation within domains of values. There are other ways to build them than the one described above for arrays. Defining approximations to data could be part of the definition of an abstract data-type, or of a class in OO programming.

_{Note: I did not expect this connection with my previous answer. hence the two separate answers.}