piclist 2009\02\05\170446a >
Thread: Agile programming (was Re: [P|C] Banksel)
face picon face 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:


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.


On Thu, Feb 5, 2009 at 3:44 AM, William Chops Westfield <spam_OUTwestfwspamspamBeGonemac.com> wrote:
{Quote hidden}

> -
<e726f69f0902051404t70568f3chd894e372b612eddd@mail.gmail.com> 7bit

In reply to: <121D19DD-3241-4D08-AC3A-6AABBDC86DC6@mac.com>
See also: www.piclist.com/techref/microchip/devprogs.htm?key=programming
Reply You must be a member of the piclist mailing list (not only a www.piclist.com member) to post to the piclist. This form requires JavaScript and a browser/email client that can handle form mailto: posts.
Subject (change) Agile programming (was Re: [P|C] Banksel)

month overview.

new search...