So, an invariant is a value which has already satified a predicate, and if it no longer satisfies one, a logic error must have occurred. On the other hand a precondition is something that must be true before being able to execute some section of code. I can se why an invariant failure should abort, but not why a precondition failure should. In particular, Wikipedia says:
If a precondition is violated, the effect of the section of code becomes undefined and thus may or may not carry out its intended work.
So, if were never to execute the section of code, the state could remain perfectly well defined. The definition does not seem to imply that the state must already be undefined. Ask yourself why the precondition is violated. Did the program fail to scrub external input enough? Or did it validate the input correctly, but
Mika Heiskanen wrote: there was a bug in a calculation following that? Where was that bug, and where might the bad value have spread since then? Is the current piece of code really the first place to encounter the bad value, or was there another place that already used it because it doesn't check preconditions as thoroughly? If you can answer all these questions at the time you decide what to do on a broken precondition (i.e. while writing the program), you should be able to pinpoint the actual error and fix it. If you can't answer them, then you can't trust the state of your program and should abort. Sebastian