From: Jacob Sparre Andersen <sparre@nbi.dk>
Subject: Re: Ada evolving towards formal analysis?
Date: Fri, 29 Jun 2012 08:57:56 +0200
Date: 2012-06-29T08:57:56+02:00 [thread overview]
Message-ID: <87r4sy4nbf.fsf@adaheads.sparre-andersen.dk> (raw)
In-Reply-To: 9fc18cdc-c3e4-4744-a193-a9c521948768@googlegroups.com
i3text@gmail.com writes:
> Is Ada going to get a prover?
I am pretty sure the intent of the ARG is that the compiler vendors can
implement an automated prover for as many of the "dynamic" predicates as
possible. Ada is a sufficiently permissible language that I expect that
there always will be correct, but statically unprovable predicates in
some real-world Ada programs.
Greetings,
Jacob
--
"I have no prejudice except against Pakistanis, which is normal."
prev parent reply other threads:[~2012-06-29 6:58 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-06-28 18:20 Ada evolving towards formal analysis? i3text
2012-06-28 20:43 ` Robert A Duff
2012-06-29 6:57 ` Jacob Sparre Andersen [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