www.piclist.com/techref/microchip/devprogs.htm?key=programming

BY : Sean Breheny email (remove spam text)

Hi Bill,

I'm not sure what type of "provable" you mean. There is very much an

ongoing effort in CS and engineering circles to have programming

languages for which one can automatically prove that functions do what

they are intended to do for all inputs. In other words, if you have a

programming language which is restrictive enough (for example, does

not allow intercommunication between functions except by explicit

parameter passing), you can then state the proposition that function

"CountWidgets(x)" always returns the correct value for any x in the

set of integers. This proposition can then be fed to an automatic

theorem prover program which can produce a mathematical proof that the

proposition is true (or false, or perhaps unable to determine).

It is also true, though, that one can prove that certain vital aspects

of a program cannot be proven true in general. For example, the

halting problem:

http://en.wikipedia.org/wiki/Halting_problem

which says that for important classes of programs and possible inputs,

it is not possible to create a general algorithm which shows whether

they terminate or loop forever.

Sean

On Thu, Feb 5, 2009 at 3:44 AM, William Chops Westfield <spam_OUTwestfwspamBeGonemac.com> wrote:

{Quote hidden}

> -

In reply to: <121D19DD-3241-4D08-AC3A-6AABBDC86DC6@mac.com>

See also: www.piclist.com/techref/microchip/devprogs.htm?key=programming