* Formal methods
@ 2021-03-25 22:16 Simon Wright
2021-03-25 22:29 ` Paul Rubin
0 siblings, 1 reply; 2+ messages in thread
From: Simon Wright @ 2021-03-25 22:16 UTC (permalink / raw)
This demonstrates to me that I will never be competent at SPARK.
https://stackoverflow.com/a/66788892/40851
^ permalink raw reply [flat|nested] 2+ messages in thread
* Re: Formal methods
2021-03-25 22:16 Formal methods Simon Wright
@ 2021-03-25 22:29 ` Paul Rubin
0 siblings, 0 replies; 2+ messages in thread
From: Paul Rubin @ 2021-03-25 22:29 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2021-03-25 22:29 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-03-25 22:16 Formal methods Simon Wright
2021-03-25 22:29 ` Paul Rubin
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox