From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!matrix.darkstorm.co.uk!reality.xs3.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: Jacob Sparre Andersen <jacob@jacob-sparre.dk>
Newsgroups: comp.lang.ada
Subject: Re: Safety of unprotected concurrent operations on constant objects
Date: Sun, 26 Oct 2014 18:11:58 +0100
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <87ioj6vjq9.fsf@adaheads.sparre-andersen.dk>
References: <slrnlm6mkg.i0l.lithiumcat@nat.rebma.instinctive.eu>
	<eT_9v.574$dr.264@fx27.iad>
	<83ha6vuynrzs.1jk08faxb8mnl.dlg@40tude.net>
	<xtDav.68151$7X2.15124@fx19.iad>
	<1jebi7cf92ak4.1trmstj8qi3wm.dlg@40tude.net>
	<zv4bv.5236$pa5.5140@fx23.iad>
	<1i6pyg077xlrv.vnwotzzgb0ut$.dlg@40tude.net>
	<nYobv.8538$116.7932@fx21.iad>
	<10pk27v48vhcb$.1qkf6roq2yzjn$.dlg@40tude.net>
	<RVObv.4489$TT7.3088@fx02.iad>
	<1qq0ryc8c4l2m.1driqwwiwwl02.dlg@40tude.net>
	<%vhcv.255737$s87.168969@fx11.iad>
	<fw1hrdv0jufx$.fetdmr8mer8o$.dlg@40tude.net>
	<qtqcv.27961$hv6.6727@fx17.iad>
	<1tb8my720vum2$.r9u7r03btzqm.dlg@40tude.net>
	<lktv6n$kit$1@loke.gir.dk>
	<8w0te2yerch4$.1ll2fpovfkuzx.dlg@40tude.net>
	<wcck39n6uut.fsf@shell01.TheWorld.com>
	<oiqjtov5sngt$.2785yqcvqig5$.dlg@40tude.net>
	<wccsiobqbru.fsf@shell01.TheWorld.com>
	<i14lhcamz6un$.10ftgndi3zl4g.dlg@40tude.net>
NNTP-Posting-Host: 151.56.102.145
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Trace: loke.gir.dk 1414343518 15240 151.56.102.145 (26 Oct 2014 17:11:58
 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Sun, 26 Oct 2014 17:11:58 +0000 (UTC)
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.4 (gnu/linux)
Cancel-Lock: sha1:MtGZyzIy7Fg9j5alExsjjkf4Q+g=
Xref: news.eternal-september.org comp.lang.ada:22764
Date: 2014-10-26T18:11:58+01:00
List-Id: <comp.lang.ada>

Dmitry A. Kazakov <mailbox@dmitry-kazakov.de> wrote:

> Sorry? There are three outcomes of a proof:
>
> 1. True
> 2. False
> 3. Don't know
>
> And two outcomes of program legality:
>
> A. Legal
> B. Illegal

Some of us see program legality slightly differently:

A. Known legal
B. Known illegal
C. Check at run-time

> Now map 1,2,3 to A,B. I assume it is:
>
> 1 -> A
> 2 -> B
> 3 -> B (cannot prove it, assume it is wrong)
>
> You?

Looking slightly differently at program legality it works out fine:

1 -> A
2 -> B
3 -> C

:-)

Greetings,

Jacob
-- 
"Be who you are and say what you feel, because those who mind
 don't matter and those who matter don't mind." -- Dr. Seuss