Message-ID:

Real programmers don't comment their code. It was hard to write, it should be hard to understand.

devel / comp.lang.ada / SPARK and pragma Export

SPARK and pragma Export

<30c383d6-bdb1-4e01-94a7-623a7532f220n@googlegroups.com>

https://www.rocksolidbbs.com/devel/article-flat.php?id=8509&group=comp.lang.ada#8509

X-Received: by 2002:a05:620a:2992:b0:6ae:e8ff:b086 with SMTP id r18-20020a05620a299200b006aee8ffb086mr11024160qkp.494.1657533925616;
Mon, 11 Jul 2022 03:05:25 -0700 (PDT)
X-Received: by 2002:a25:d714:0:b0:66f:5898:9eb1 with SMTP id
o20-20020a25d714000000b0066f58989eb1mr828451ybg.633.1657533925110; Mon, 11
Jul 2022 03:05:25 -0700 (PDT)
Path: i2pn2.org!i2pn.org!usenet.blueworldhosting.com!feed1.usenet.blueworldhosting.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Mon, 11 Jul 2022 03:05:24 -0700 (PDT)
Injection-Info: google-groups.googlegroups.com; posting-host=220.235.61.37; posting-account=re0iSwoAAABjnUZ19gwmNR9Cx_O9p1jK
NNTP-Posting-Host: 220.235.61.37
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <30c383d6-bdb1-4e01-94a7-623a7532f220n@googlegroups.com>
Subject: SPARK and pragma Export
From: liam@liampwll.com (Liam Powell)
Injection-Date: Mon, 11 Jul 2022 10:05:25 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Received-Bytes: 1305

by: Liam Powell - Mon, 11 Jul 2022 10:05 UTC

I'm wondering exactly how SPARK works with pragma Export, specifically exported procedures that may be called by multiple threads. Is SPARK capable of reasoning about procedures that are called externally, and if so is there a way to inform it about potential simultaneous calls?