* 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