From: Paul Rubin <no.email@nospam.invalid>
Subject: Re: Formal methods
Date: Thu, 25 Mar 2021 15:29:15 -0700 [thread overview]
Message-ID: <87wnturhok.fsf@nightsong.com> (raw)
In-Reply-To: ly35wij2vt.fsf@pushface.org
Simon Wright <simon@pushface.org> 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.
prev parent reply other threads:[~2021-03-25 22:29 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2021-03-25 22:16 Formal methods Simon Wright
2021-03-25 22:29 ` Paul Rubin [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox