From: "Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>
Subject: Re: Beside of SPARK: how do you compare Alt-Ergo and Coq?
Date: Tue, 21 Feb 2012 23:10:30 +0100
Date: 2012-02-21T23:10:30+01:00 [thread overview]
Message-ID: <op.v91ujsk2ule2fv@douda-yannick> (raw)
In-Reply-To: op.v90efmcbule2fv@douda-yannick
Le Tue, 21 Feb 2012 04:24:48 +0100, Yannick Duchêne (Hibou57)
<yannick_duchene@yahoo.fr> a écrit:
> how do you compare both?
The main topic is that Coq cannot be easily used with language others than
SML/OCaml and Haskell, while Alt-Ergo uses comments as annotations in
source, like SPARK do. But I could not know how exactly SPARK is linked to
Alt-Ergo, nor I could find any tiny example of Ada source proved with
Alt-Ergo.
If any one know some tiny practical examples of Ada+Alt‑Ergo, any pointers
are welcome.
Another question may be: do Alt-Ergo for Ada depends on SPARK or can be
independent from SPARK?
--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University
next prev parent reply other threads:[~2012-02-21 22:10 UTC|newest]
Thread overview: 4+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-02-21 3:24 Beside of SPARK: how do you compare Alt-Ergo and Coq? Yannick Duchêne (Hibou57)
2012-02-21 15:57 ` Yannick Duchêne (Hibou57)
2012-02-21 22:10 ` Yannick Duchêne (Hibou57) [this message]
2012-02-23 19:08 ` Phil Clayton
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox