Next: Assert, Previous: Introduction, Up: Introduction
The Nana project was inspired by some other projects, in particular:
Anna is a language for formally specifying the intended behaviour of Ada programs. It extends Ada with various different kinds of specification constructs from ones as simple as assertions, to as complex as algebraic specifications. A tool set has been implemented at Stanford for Anna, including:
- standard DIANA extension packages, parsers, pretty-printers;
- a semantic checker;
- a specification analyser;
- an annotation transformer; and
- a special debugger that allows program debugging based on formal specifications
All tools have been developed in Ada and are therefore extremely portable. Anna has thus been ported to many platforms. For more information send e-mail to "anna-request@anna.stanford.edu". Before down loading the huge Anna release, you may wish to copy and read some Anna LaTeX reports.
Anna is available from: ftp://anna.stanford.edu/pub/anna
Eiffel is a pure object-oriented language featuring multiple inheritance, polymorphism, static typing and dynamic binding, genericity (constrained and unconstrained), a disciplined exception mechanism, systematic use of assertions to promote programming by contract, and deferred classes for high-level design and analysis.
See "A Practical Approach to Programming with Assertions" in Vol 21, No. 1, January 1995 of IEEE Transactions on Software Engineering for an interesting paper describing APP. Unfortunately the APP tool doesn't seem to be freely available (I'm willing to be corrected on this). Note that any similarity between my examples and David's are due to morphic resonance.
To quote from http://www.sunlabs.com/research/adl/
:
ADL (Assertion Definition Language) is a specification language for programming interfaces. It can be used to describe the programmer's interface to any C-callable function, library or system call.The Practical Specification Language.
ADL is the world's most practical specification language because:
- Even partial specifications are useful
- Test programs can be automatically generated from ADL specifications
- Specifications are external to the implementation of the interface, so that they are vendor-independent.
An Automated Test Generator.
An ADL specification is not just a paper document. It can be compiled by ADLT (the ADL translator). ADLT generates:
- Header files, that can be used in an implementation
- Test programs, that ensure that any implementation meets the specification
- Natural-language documentation, derived directly from the specification
ADLT can be used:
As a test generator, to create tests for existing software or for existing standards As a development tool, to ensure that documentation, software, and tests are aligned, and to enable concurrent work on all three aspects of software production.
Nana is essentially a poor mans implementation of some of these ideas which works for C and C++. Ideally in the best of all possible worlds you might want to look at Eiffel or in the military world Ada and Anna. If you use TCL/TK you might also be interested in Jon Cook's ‘AsserTCL’ package.