* Ada evolving towards formal analysis?
@ 2012-06-28 18:20 i3text
2012-06-28 20:43 ` Robert A Duff
2012-06-29 6:57 ` Jacob Sparre Andersen
0 siblings, 2 replies; 3+ messages in thread
From: i3text @ 2012-06-28 18:20 UTC (permalink / raw)
I have been reading about SPARK, and about related systems like Spec#, JML, ACSL/Frama-c, and Escher C Verifier. These systems basically add type constraints, design by contract, and a prover to support code verification.
Now I see that Ada 2012 is incorporating some part of design by contract. How far is it intended to make Ada implementations (e.g. GNAT) like the things mentioned above? Is Ada going to get a prover?
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: Ada evolving towards formal analysis?
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
1 sibling, 0 replies; 3+ messages in thread
From: Robert A Duff @ 2012-06-28 20:43 UTC (permalink / raw)
i3text@gmail.com writes:
> I have been reading about SPARK, and about related systems like Spec#,
> JML, ACSL/Frama-c, and Escher C Verifier. These systems basically add
> type constraints, design by contract, and a prover to support code
> verification.
>
> Now I see that Ada 2012 is incorporating some part of design by
> contract. How far is it intended to make Ada implementations
> (e.g. GNAT) like the things mentioned above? Is Ada going to get a
> prover?
AdaCore is working on such things.
- Bob
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: Ada evolving towards formal analysis?
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
1 sibling, 0 replies; 3+ messages in thread
From: Jacob Sparre Andersen @ 2012-06-29 6:57 UTC (permalink / raw)
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."
^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2012-06-29 6:58 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
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 is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox