From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.5-pre1 (2020-06-20) 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.5-pre1 Path: eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail From: Paul Rubin Newsgroups: comp.lang.ada Subject: Re: Formal methods Date: Thu, 25 Mar 2021 15:29:15 -0700 Organization: A noiseless patient Spider Message-ID: <87wnturhok.fsf@nightsong.com> References: Mime-Version: 1.0 Content-Type: text/plain Injection-Info: reader02.eternal-september.org; posting-host="835598ae6c6981d3d35b1665ade1362a"; logging-data="12437"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+LzKSJOkoOkW3d+5CfPbhl" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (gnu/linux) Cancel-Lock: sha1:KOSw2+nvbpYH8lu8cHTreh3m5/Q= sha1:OLvLh6lVWm/O0+7rLY0H+o8cTtw= Xref: reader02.eternal-september.org comp.lang.ada:61655 List-Id: Simon Wright writes: > This demonstrates to me that I will never be competent at SPARK. > https://stackoverflow.com/a/66788892/40851 There is some further discussion of those techniques here: https://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_investigate_unproved_checks.html I remember a more tutorial document from a while back, but can't easily find it right now. It showed an example of a Coq proof connected up to SPARK. It probably helps to have studied some basic mathematical logic (proof theory) before getting into this SPARK stuff. That makes it flow fairly naturally.