From: Mark Lorenzen <mark.lorenzen@gmail.com>
Subject: Re: SPARK: Problem with using constants in a post annotation
Date: Mon, 17 Jan 2011 08:13:38 -0800 (PST)
Date: 2011-01-17T08:13:38-08:00 [thread overview]
Message-ID: <3d8c0e1a-79e1-4fda-a434-7cfcbac30977@m7g2000vbn.googlegroups.com> (raw)
In-Reply-To: b5e815ae-658c-4c86-8b2d-e91b11422b82@f35g2000vbl.googlegroups.com
On 17 Jan., 16:17, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
> Looks like this wish has been answered. Adacore have just announced a
> new version of SPARK GPL.
>
> The main change is the preview of the SPARKBridge technology which
> allows SMT solvers to be used along with the Simplifier. The release
> note says that this error in VC generation has been fixed.
>
> Cheers,
>
> Phil
Fantastic! I'm also very happy about J812-010 "Improve reasoning with
unit range quantified conclusions". Any improvement that helps the
user write (and discharge) loop invariants is very welcome.
- Mark L
next prev parent reply other threads:[~2011-01-17 16:13 UTC|newest]
Thread overview: 8+ messages / expand[flat|nested] mbox.gz Atom feed top
2011-01-13 9:18 SPARK: Problem with using constants in a post annotation George
2011-01-13 9:26 ` George
2011-01-13 11:15 ` Phil Thornley
2011-01-13 12:23 ` George
2011-01-17 11:08 ` Mark Lorenzen
2011-01-17 15:17 ` Phil Thornley
2011-01-17 16:13 ` Mark Lorenzen [this message]
2011-01-13 11:15 ` George
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox