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

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?

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=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.

StackExchange Computer Science Q#27597, answer score: 5