Saying when does not mean completion

Got it! This site "creationpie.com" uses cookies. You consent to this by clicking on "Got it!" or by continuing to use this website. Note: This appears on each machine/browser from which this site is accessed.

In computational program correctness theory, "when" does not imply that one will actually get there. That is, "when the program stops" does not mean the program will actually stop. A useful analogy is the distinction between partial correctness and total correctness.

When pouring, for example, sugar for someone into their tea or coffee, one says to them "say when". That is, "let me know when I have poured enough" or "let me know when to stop pouring".

What happens if the person never says "when"?

The computational ideas of partial and total correctness can help understand these ideas.

Testing of programs cannot be used to show a program is correct (according to some specification).

Details are left as a future topic.

The only way to show a program correct is by using logical reasoning (and induction) in an area of what is called program correctness or program verification and validation.

Partial correctness means that when the program stops, the desired result is achieved.

Total correctness means that the program is partially correct and, in addition, does stop.

Total correctness is harder to show than partial correctness. (Why?).

To informally show total correctness one observes (the math gets more involved) that progress is made towards the goal during each loop body iteration so that eventually the loop will stop.

Let us look at a simple programming example. The Lua programming language is used.

Here is a Lua program to count from 1 to 4. During each loop iteration, the variable pos1 is incremented by 1.

Here is the Lua code [#1]

local pos1 = 0
local len1 = 4
while pos1 ~= len1 do
	pos1 = pos1 + 1
	end
print(string.format("done at %d",pos1))

Here is the output of the Lua code.

done at 4

When the loop ends, the output is "done at 4".

Let us now remove the increment of variable pos1.

Here is the Lua code [#2]

local pos1 = 0
local len1 = 4
while pos1 ~= len1 do
	end
print(string.format("done at %d",pos1))

The code is still partially correct in that when the loop ends, the output is "done at 4". But the loop never ends. So the loop is partially correct but not totally correct. Here is the output of the Lua code.
There is no output since the program never ends.

Alan Turing (1912-1954) developed the ideas that proved the limits of computing before the first programmable digital computer was built. Claude Shannon (1939) showed that one could built such a computer.
The halting problem (Turing, Turing machine, 1936) result: It is impossible to write a computer program that looks at another computer program (and its data) and determines whether that other computer program eventually halts.

The possible answers for a computation of an undecidable problem are yes (true), no (false), or maybe (wait forever). One may be able to go "outside the system" to determine a better answer.

An abstract (or physical) computer can be called a Turing Machine. A Turing complete programming language can compute any computable function.

[waiting for a program to stop, secure form submission, virus detection]

More: Alan Turing: halting problem