Martin wrote:
You’re forgetting the customer. Customers want speed and are often willing to pay for it. Yes, ships are slow, but how much lower speed would customers be willing to accept?
They are willing to pay for aircraft speed, otherwise it doesn’t matter, international shipping takes 2-3 months regardless. At those speeds what’s important is planning. 5-10 years ago large vessels traveled at 25 or more knots. Today they travel at 20. The speed is just an optimization of cost.
Martin wrote:
Software I use would have found that one (and it wouldn’t even need a formal specification, arithmetic overflows are by default treated as undesirable). Well, unless I decided it wasn’t desirable to check for it. Otherwise it would have “forced” me to account for that possibility. The issue with this approach is that you can have a significant amount of additional code.
Most formal methods do not check for overflow. That would not be in the “requirements specifications”, so to say. The B-Method which was used in the Paris Metro Line 14 project is an exception — it does check for overflow.
(For the record, Formal Methods is my main area of professional expertise. I have worked in it both as an academic and as an industrial practitioner.)
Airborne_Again wrote:
Most formal methods do not check for overflow. That would not be in the “requirements specifications”, so to say. The B-Method which was used in the Paris Metro Line 14 project is an exception — it does check for overflow.
As I wrote, it wouldn’t even need a formal specification for this. I wrote that tool myself. It checks for them because I consider overflows to be embarrassing. I usually don’t want it and if that’s the case, it shouldn’t be possible. The same goes for division by zero. And it depends on the language/ platform. One has to love compiler optimizations in C for example. 
LeSving, I’ll take your word for it that the change in speed would be insignificant to the customers and the saving would go to the bottom line. On a related note, I sure would like something between a ship (too slow) and an aircraft (often unnecessarily expensive).
