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 typechecking of various sorts.
But typesafety 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
> "nearoptimal" 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; DavidJoerg 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>2body problems)
> >can't be analyzed without computation, so there are two choices.
> >
> >The topdown 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 bottomup 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 topdown thinkers are unsuccessfully trying to make correctness
> >provable,
> >the bottomup thinkers are successfully making correctness more probable.
> >
> >Steve
> >
>
More information about the Squeakdev
mailing list
