From: "Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>
Subject: “Why Hi-Lite Ada?” (paper)
Date: Sat, 01 Oct 2011 11:17:06 +0200
Date: 2011-10-01T11:17:06+02:00 [thread overview]
Message-ID: <op.v2n1esn3ule2fv@index.ici> (raw)
An up to date paper about Ada, oriented towards Design By Contract (™) and
proofs to be runtime-error-free. Noticeably, the paper is hosted at
research.microsoft.com. It goes beyond just SPARK, by introducing some
other ways to prove correctness of Ada programs (to get multiple choices
is sometime better), including Alt-Ergo and the Why system. The paper was
written in the context of a so called “First International Workshop On
Intermediate Verification Languages”.
Date: 2011
Length: 13 pages
Authors: Jérôme Guitton, Johannes Kanig and Yannick Moy
Document:
http://research.microsoft.com/en-us/um/people/moskal/boogie2011/boogie2011_pg27.pdf
Enjoy :-)
--
“Syntactic sugar causes cancer of the semi-colons.” [Epigrams on
Programming — Alan J. — P. Yale University]
“Structured Programming supports the law of the excluded muddle.” [Idem]
Java: Write once, Never revisit
reply other threads:[~2011-10-01 9:17 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox