From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on
	ip-172-31-74-118.ec2.internal
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=3.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.6
Path: eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Ada and software testing
Date: Wed, 14 Jul 2021 13:02:23 -0700
Organization: A noiseless patient Spider
Message-ID: <87h7gwy88g.fsf@nightsong.com>
References: <871r84cq4r.fsf@nightsong.com>
	<5bc2434a-6784-47d6-ba66-50edff4f80f0n@googlegroups.com>
	<87pmvky9lz.fsf@nightsong.com> <scnf8n$1lgd$1@gioia.aioe.org>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org; posting-host="158c5d4bee3779fbf0a272d27e09ef8a";
	logging-data="6444"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18O2E0LVLIO60iBxU1f38Uf"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (gnu/linux)
Cancel-Lock: sha1:sTMxMHbIGCKEd1LAig7f3J2pRkk=
	sha1:nvus6uljX4xJBajw+O9FjMKPa9A=
Xref: reader02.eternal-september.org comp.lang.ada:62382
List-Id: <comp.lang.ada>

"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.