From: Jacob Sparre Andersen <jacob@jacob-sparre.dk>
Subject: Ada 2012 talk at DANSAS'13
Date: Thu, 15 Aug 2013 10:39:59 +0200
Date: 2013-08-15T10:39:59+02:00 [thread overview]
Message-ID: <87mwojxs80.fsf@adaheads.sparre-andersen.dk> (raw)
I've gotten a talk on Ada 2012 accepted for the Danish Static Analysis
Symposium (DANSAS'13) Friday August 23rd in Odense. The title and
abstract are:
Contract-based Programming with Ada 2012 - an experience report
The 2012 version of the Ada programming language standard includes
checked "contracts" and "aspects" for subprograms and types. Some of
these are by definition checked at compile-time, while other checks
can be postponed to run-time, if a static analysis is unfeasible (or
just not implemented).
At AdaHeads, we are currently developing a hosted telephone reception
system, where the core component is written in Ada 2012. We picked
Ada 2012 specifically to be able to use the contracts and aspects to
increase our confidence that the software is correct.
Our experience so far is that GNAT-GPL-2013 (the only generally
available Ada 2012 compiler) only implements static (compile-time)
checking of contracts and aspects where it is required by the
language standard. This means that for now, the big static analysis
benefits of using Ada are related to the basic type system, which
also existed in earlier versions of the standard, and the major
benefit of switching to Ada 2012 at the moment is in the improved
run-time checks.
General information on DANSAS'13 can be found at:
http://dansas.sdu.dk/2013/
Greetings,
Jacob
--
PNG: Pretty Nice Graphics
next reply other threads:[~2013-08-15 8:39 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2013-08-15 8:39 Jacob Sparre Andersen [this message]
2013-08-15 10:33 ` Ada 2012 talk at DANSAS'13 Paul Rubin
2013-08-15 13:02 ` SPARK vs. Ada 2012 for static analysis (Was: Ada 2012 talk at DANSAS'13) Jacob Sparre Andersen
2013-08-15 14:01 ` Shark8
2013-08-15 17:18 ` SPARK vs. Ada 2012 for static analysis Paul Rubin
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox