From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,20a383dc7abacbdf,start
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.68.196.232 with SMTP id ip8mr2757232pbc.6.1340907724968;
        Thu, 28 Jun 2012 11:22:04 -0700 (PDT)
Path: 
 l9ni30419pbj.0!nntp.google.com!news1.google.com!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
From: i3text@gmail.com
Newsgroups: comp.lang.ada
Subject: Ada evolving towards formal analysis?
Date: Thu, 28 Jun 2012 11:20:01 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: <9fc18cdc-c3e4-4744-a193-a9c521948768@googlegroups.com>
NNTP-Posting-Host: 75.170.63.109
Mime-Version: 1.0
X-Trace: posting.google.com 1340907724 25132 127.0.0.1 (28 Jun 2012 18:22:04
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Thu, 28 Jun 2012 18:22:04 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=75.170.63.109;
 posting-account=_xNmGgoAAADzVbG1LIrTaXAR97KD43ZC
User-Agent: G2/1.0
Content-Type: text/plain; charset=ISO-8859-1
Date: 2012-06-28T11:20:01-07:00
List-Id: <comp.lang.ada>

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?