[LINK] Ada programming language security

Glen Turner gdt at gdt.id.au
Sun Dec 30 10:57:08 AEDT 2012


On 21/12/12 12:21, stephen at melbpc.org.au wrote:
> The new version of Ada allows developers to do contract-based programming

You can write object-oriented COBOL too. The more add-ons like these the
less the coherence of the language, and eventually it becomes unwieldy.

The use of invariant pre- and post-conditions isn't as straightforward
as it at first appears, which is one of the reasons that it has failed
to catch on. In particular, stating the post-conditions in terms of the
per-conditions which allow for non-trivial unit testing isn't at all
simple, doubly so for functions with side-effects such as I/O.
Test-oriented development can reap the gains of contract-driven
programming and more. Of course the two can be complementary, you don't
have to forsake one to use the other.

Invariants are a popular approach within academia, and rightly so as it
leads to an interesting way to reason about programs without getting
caught up in their procedural detail. In critical systems we need to be
able to reason about programs, so they are often used there. The problem
is the low productivity of critical systems code, and yet the explosion
of lines of code in avionics and combat software. We want to have to
prove as few lines of code as possible, and then to tackle proofs
closely related to the problem rather than to the operation of the language.

Also, the ability to state an invariant in the syntax of the language is
the least of the requirements -- if Ada were more expressive it could be
done with a function call. What is also needed is a way to get to the
invariant statements without detailed parsing of the program, because
then it is easy to write programs to reason about programs. As Ada is a
compiled language getting to the invariants isn't simple at all, and
varies by compiler product.

US DoD seem quite taken with Ada, and yet it's a poor tool for critical
systems because it makes explicit things which are best left implicit.
Something which is implicit needs to be proven once (when the language
is implemented), something which is explicit needs to proven with each
use. For example, the lack of iterators in Ada meant that every loop had
to be proven. Ada has also got explicit locking and explicit
parallelism, and there's no reason for either of those in a modern
programming language -- we know can use transactional memory to avoid
explicit locking and we can use goal-driven functional programming to
avoid explicit parallelism.

In my view people are far too taken with the determinism of a fully
compiled language with no run-time support. This does make reasoning
about simple programs easier, but Ada isn't meant to be about simple
programs. Complex embedded code should require run-time support (garbage
collection, transactional memory, linked stacks, etc) because the
benefits in correctness of the application are well worth it.

-glen

-- 
Glen Turner   www.gdt.id.au/~gdt



More information about the Link mailing list