Ada evolving towards formal analysis?

Ada evolving towards formal analysis?

[i3text]

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?

Re: Ada evolving towards formal analysis?

[Robert A Duff]

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

Re: Ada evolving towards formal analysis?

[Jacob Sparre Andersen]

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."