Re: correctness of physics function

<bob@xxxxxxxxxxxxxx> wrote in message
news:1175072079.217427.61190@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
I wrote a function for a physics simulation to try to figure out the
force that an object bounces off a wall with assuming conservation of
kinetic energy. It seems to work, but I was wondering if anyone has
any ideas on how to prove its correctness.

It is shown below:
[snip code]

I think you are overestimating the usefulness of proving the
correctness of programs, and/or underestimating the difficulty.

To prove the correctness of a function, you need to first formally
specify the intended behaviour of the function. As stated, your function
is probably incorrect, because in physics, we either have a concept of
significant digits in measurements, or we assume that all measurements are
exact. Your code does not implement any concept of significant digits, and
it does not perform infinite-precision arithmetic. The fact that it does a
100-iteration binary search is somewhat discouraging as well.

- Oliver


.