From: i3text@gmail.com
Subject: Ada evolving towards formal analysis?
Date: Thu, 28 Jun 2012 11:20:01 -0700 (PDT)
Date: 2012-06-28T11:20:01-07:00 [thread overview]
Message-ID: <9fc18cdc-c3e4-4744-a193-a9c521948768@googlegroups.com> (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?
next reply other threads:[~2012-06-28 18:22 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-06-28 18:20 i3text [this message]
2012-06-28 20:43 ` Ada evolving towards formal analysis? Robert A Duff
2012-06-29 6:57 ` Jacob Sparre Andersen
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox