Path: utzoo!attcan!uunet!cs.utexas.edu!usc!ucsd!helios.ee.lbl.gov!pasteur!yew.Berkeley.EDU!faustus
From: faustus@yew.Berkeley.EDU (Wayne Christopher)
Newsgroups: comp.object
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <21140@pasteur.Berkeley.EDU>
Date: 12 Jan 90 19:47:31 GMT
Sender: news@pasteur.Berkeley.EDU
Reply-To: faustus@yew.Berkeley.EDU (Wayne Christopher)
Organization: University of California at Berkeley
Lines: 25

> Suppose I specify an square root function "sqrt" by:
> 
>     abs( sqrt( x ) ** 2 - x ) < 0.01
> 
> I claim this is a good specification (modulo the [...]) of the behaviour of
> "sqrt". Now tell me how you're going to generate code for sqrt from it, and
> convince me that the code will be efficient, and that you have a *general*
> mechanism that will do this for examples further removed from the Opening
> Book of moves in the Specification Game.

You've stated a constraint on the possible values of sqrt(x), and since
sqrt is a reasonably well-behaved function, you could hand this to a
constraint-solving system, and if it's good enough, it would probably
solve it by Newton's method.  In general, if your constraints (or
specifications) are numeric, and your functions are differentiable, it's
possible to solve them in this way.  Of course, many programming problems
are non-numeric, and much more difficult than this one.

Speaking of constraint-solving systems, has anybody had any experience
using constraint logic programming (CLP) systems?  Alan Borning at U.
Washington is working on this stuff, and so are some people at Monash
University in Australia.  Is there anybody else?  Has CLP been applied
to any real problems?

	Wayne