* “Why Hi-Lite Ada?” (paper)
@ 2011-10-01 9:17 Yannick Duchêne (Hibou57)
0 siblings, 0 replies; only message in thread
From: Yannick Duchêne (Hibou57) @ 2011-10-01 9:17 UTC (permalink / 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
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2011-10-01 9:17 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2011-10-01 9:17 “Why Hi-Lite Ada?” (paper) Yannick Duchêne (Hibou57)
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox