[vox-tech] loop never exits!

Brian Lavender brian at brie.com
Thu Apr 22 20:47:10 PDT 2010


On Thu, Apr 22, 2010 at 09:15:10AM -0700, Brian Lavender wrote:
> On Thu, Apr 22, 2010 at 09:03:23AM -0500, Chanoch (Ken) Bloom wrote:
> > 
> > The following idiom must be used instead:
> > 
> > int* iterator=thearray+itssize;
> > while( iterator-- > thearray){
> >   /* do something with the iterator. */
> > }
> > 
> 
> Very nice. If we had a "Hoare" karma point, I would definitely
> think that this deserves one. 
> 
> Trivia question. 
> 
> What is the link between Charles Hoare and Bertrand Meyer?

Thanks to everyone for their help on this thread. The input certainly
has been helpful and if anything has been a catalyst to consider various
aspects of my code and programming. I am once again one step closer to
finishing my MS Project, assuming the project will eventually terminate!

So, Bertrand Meyer developed Design by Contract, or perhaps coined the
term. It is one of the foundations of Eiffel. 

And, Tony Hoare developed Hoare Logic which can be defined by the
triple {P} C {Q} where P is the set of preconditions,  Q is the set of
postconditions, and C is the set of commands. Using Axioms and inference
rules, one can prove his code correct. This of course proves partial
correctness. For total correctness, one needs to prove termination. So,
the link is that the precondition is {P} in Eiffel and {Q} is the post
condition. 

I took Formal Methods with Dr. Cui Zhang last semester at Sac State,
so this stuff is fresh in my head, assuming I got it right.

brian
-- 
Brian Lavender
http://www.brie.com/brian/

"There are two ways of constructing a software design. One way is to
make it so simple that there are obviously no deficiencies. And the other
way is to make it so complicated that there are no obvious deficiencies."

Professor C. A. R. Hoare
The 1980 Turing award lecture


More information about the vox-tech mailing list