Ada 2012 talk at DANSAS'13

Ada 2012 talk at DANSAS'13

[Jacob Sparre Andersen]

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

Re: Ada 2012 talk at DANSAS'13

[Paul Rubin]

Jacob Sparre Andersen <jacob@jacob-sparre.dk> writes:
>    Our experience so far is that GNAT-GPL-2013... only implements
>    static (compile-time) checking of contracts and aspects where it is
>    required by the language standard.

Does SPARK-2014 help?  I'm not sure if it exists yet, but I gather
GNATProve (which is out there) is some kind of precursor to it.

Disclaimer: I'm interested in trying this stuff out, but I don't really
know anything about it yet, beyond having looked at a few web pages.

SPARK vs. Ada 2012 for static analysis (Was: Ada 2012 talk at DANSAS'13)

[Jacob Sparre Andersen]

Paul Rubin wrote:

> Does SPARK-2014 help?  I'm not sure if it exists yet, but I gather
> GNATProve (which is out there) is some kind of precursor to it.

SPARK would of course give compile/analysis-time checking, but we don't
consider it appropriate for the project.  The cost of implementing
sockets and containers in SPARK alone would probably kill that idea.

I'm not sure SPARK-2014 wasn't announced when we started the project,
and I don't consider it ready for real-life use yet, as tasking isn't
covered yet.

We want as much static analysis as we can get, but we are at the same
time working in a context where the value of making an "absolutely
perfect" application isn't that much bigger than writing a "definitely
above average reliability" application.  The whole system also depends
on other parts, which may fail too.  As long as we have a few orders of
magnitude fewer failures than the other parts, we are quite happy.

As I see things, the important place for complete static analysis
(i.e. SPARK) is in components which have a unique possibility of
breaking your system.  One obvious example is a PRNG used for
cryptography; if it is broken, your whole system is broken, and nothing
else can break the system in quite the same way.

Greetings,

Jacob
-- 
»You know the world has gone crazy when the best rapper is a
 white guy, the best golfer is a black guy, the swiss hold
 the America's cup, France is accusing the U.S. of
 arrogance, and Germany doesn't want to go to war«

Re: SPARK vs. Ada 2012 for static analysis (Was: Ada 2012 talk at DANSAS'13)

[Shark8]

On Thursday, August 15, 2013 7:02:17 AM UTC-6, Jacob Sparre Andersen wrote:
> 
> As I see things, the important place for complete static analysis
> (i.e. SPARK) is in components which have a unique possibility of
> breaking your system.  One obvious example is a PRNG used for
> cryptography; if it is broken, your whole system is broken, and nothing
> else can break the system in quite the same way.

I see what you're saying, but I [somewhat] disagree: the scope you're using is too small. it's the small "everybody uses it and assumes it's correct" things that need SPARK-verification.

Take DNS for example: there's a *lot* of bugs that have been found in any main DNS0server over the past decade [or two]. Everybody using the internet is interacting with a DNS, even if indirectly. And so it behooves us to eliminate everything [bug-wise] that we can -- which is what formal verification does, and it's what the twp guys who developed Ironsides did. ( http://ironsides.martincarlisle.com/ )

The two papers linked just above the "Download" heading are quite informative and say things much better than I can.

I would love to see a formally-verified OS, and to be honest MS would have a much better product to sell if they did so to their OS instead of worrying about "looking stylish". (See the Windows 8 disaster)

Re: SPARK vs. Ada 2012 for static analysis

[Paul Rubin]

Jacob Sparre Andersen <jacob@jacob-sparre.dk> writes:
> As I see things, the important place for complete static analysis
> (i.e. SPARK) 

I didn't have the impression SPARK does -complete- static analysis, but
just that it did more than plain Ada does.  You have a reasonable amount
of control over what it does statically.