HELP! formalizing OO

Lex Spoon lex at cc.gatech.edu
Tue Apr 28 16:40:27 UTC 1998


Though it's infeasible to prove a program correct, how about proving
things like "consistent" or "safe"?  Even if it's too hard to prove
that a robot arm will build a car, it would seem reasonable to prove
things like, the arm doesn't start drilling holes in itself or in
nearby workers.

To an extent this is already done via type-checking of various sorts.
But type-safety is a pretty weak constraint.

Such things wouldn't give you a proof of correctness in a traditional
sense, but they would you help convince *yourself* that a program is
likely to work properly.


Lex



Jarvis, Robert P. writes:
 > I think this is an interesting topic.  Being able to come up with a
 > proof of a given programs correctness would be wonderful, but I think
 > this is often impractical in the "real world".  To be able to prove that
 > a program will behave correctly you have to define what the correct
 > behaviors are, and in many cases the definition of "correct behavior" is
 > a moving target.  So you may be able to prove that a program meets a set
 > of specifications which existed at some time, but can you then prove
 > that the specifications are correct?  The chicken and the egg trade
 > places, the wyrm devours its tail, and we 
 > iterate again.  :-)  There's also an analogy here to solving some
 > production optimization problems which are at once too complex and too
 > loosely defined for solution by traditional methods.  What you find is
 > that although you may not be able to determine the "optimal" solution, a
 > "near-optimal" solution is good enough and requires a fraction of the
 > computation time.  In software I think that providing an environment
 > where correctness is probable, if not provable, is probably the "near
 > enough" solution.
 > 
 > Bob Jarvis
 > The Timken Company
 > 
 > >-----Original Message-----
 > >From:	Steve Dekorte [SMTP:steve at inquisit.com]
 > >Sent:	Monday, April 27, 1998 8:39 PM
 > >To:	squeak at cs.uiuc.edu; dnelson at redwoodsoft.com; David-Joerg at deshaw.com
 > >Cc:	The recipient's address is unknown.
 > >Subject:	Re: HELP! formalizing OO
 > >
 > >
 > >Florin wrote:
 > >>..I would say though that math looks to me like it
 > >>is still ticking,
 > >
 > >An interesting thing about math/logic is that it can prove some of
 > >it's own limitations.
 > >
 > >I think I remember hearing about proofs of the insolvability of the n>2 body
 > >problem
 > >and of general solutions to finding the roots of polynomials above a certain
 > >order.
 > >
 > >If these problems are provably insolvablable, should we have much
 > >confidence in what seem to be the more complex problems of large programs
 > >being solvable? (By solvable I mean knowing everything about what they
 > >do without actually running them)
 > >
 > >I think most everyone sees that complex programs (like n>2-body problems)
 > >can't be analyzed without computation, so there are two choices.
 > >
 > >The top-down approach is to attempt to make programming langagues more
 > >analyzable before computation (Strong typing, etc) so correctness can be
 > >proven.
 > >This approach is basically out to eliminate the dynamic aspects of the system
 > >that lead to complexity. (Of course if Smalltalk can be written in ADA, how
 > >is ADA more provably correct or "safe"?)
 > >
 > >The bottom-up approach is to look for new ways of managing complexity so
 > >correctness
 > >is more probable. OO of the Smalltalk type is, IMO, an example of the 2nd
 > >approach.
 > >It looks at real the source of chaos - excessively coupled equations (via
 > >variables)
 > >and structures the langauge to make this problem easier to avoid.
 > >
 > >So while the top-down thinkers are unsuccessfully trying to make correctness
 > >provable,
 > >the bottom-up thinkers are successfully making correctness more probable.
 > >
 > >Steve
 > >
 > 





More information about the Squeak-dev mailing list