I know that there is something called partial correctness, but I was wondering i

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?

Explanation / Answer

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

Related Questions

Navigate

• Browse (All)
• Browse I
• Subjects

Integrity-first tutoring: explanations and feedback only — we do not complete graded work. Learn more.