Re: Ada and software testing

[Paul Rubin <no.email@nospam.invalid>]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>> I do have to say that errors thrown by runtime checks on range types are
>> still program bugs,
> No, it depends on the contract.

If a contract is broken by either the caller or the callee, it is a
program bug either way, I would have thought.

>> in the sense that they are type errors,
> A type error cannot happen at run-time per definition of strong
> typing. Constraint violation is not a type error.

Hmm ok, if out of range for a range type is considered a constraint
error rather than a type error, then it's ok to say the compiler can't
check it even in principle, and it becomes the responsibility of the
application user or environment.  Inputs that trigger a constraint error
might be considered invalid in some situations.

> If you can. In reality it is impossible to enforce validity per type
> system, because such contracts are often not enforceable.

Yep.  SPARK tries to enforce such constraints at compile time, but it's
not always possible to use it.