comp.lang.ada
 help / color / mirror / Atom feed
From: moy@adacore.com
Subject: Re: [Spark] Proving GCD
Date: Wed, 5 Apr 2017 16:52:44 -0700 (PDT)
Date: 2017-04-05T16:52:44-07:00	[thread overview]
Message-ID: <b547d2c7-2686-4281-90cf-b22e56734d4e@googlegroups.com> (raw)
In-Reply-To: <58caf63b$0$24793$426a74cc@news.free.fr>

Hi Fred,

I had proved various versions of GCD some time ago, and needed some motivation to write a blog post about it. Your question gave me the impulse! Here is the blog post, that should answer your question: 

http://www.spark-2014.org/entries/detail/gnatprove-tips-and-tricks-proving-the-ghost-common-denominator-gcd

Cheers

  parent reply	other threads:[~2017-04-05 23:52 UTC|newest]

Thread overview: 10+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2017-03-16 20:31 [Spark] Proving GCD Frédéric Praca
2017-03-17  1:20 ` Brian Kolden
2017-03-17  9:07   ` Frédéric PRACA
2017-04-05 23:52 ` moy [this message]
  -- strict thread matches above, loose matches on Subject: below --
2017-03-16 20:27 Frédéric Praca
2017-03-17  9:33 ` Frédéric PRACA
2017-03-17 13:00   ` Phil Thornley
2017-03-17 13:24     ` Frédéric PRACA
2017-03-17 13:28       ` Frédéric PRACA
2017-03-17 17:16         ` Phil Thornley

replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox