Jacob Sparre Andersen

Contract-based programming is a software development technique, where you include assertions of program properties as a part of the compiled source text. In the strict form, the assertions are checked at compile-time, but in this presentation I will focus on the more common, less strict, form, where at least some of the assertions aren't checked until run-time. Ada gives us a lot of help, so we can write the our assertions about the program properties once, and then have the compiler insert actual run-time checks wherever there is a possibility that the assertion is violated.

This presentation will focus on how we can write these contracts in Ada in a way that make them effective at ensuring that our source text does what we intend it to and allow the compiler to generate efficient checks of the assertions. The intended audience is anybody with enough programming experience to know concepts like types, encapsulation and packages. Having tried to write Ada before will be a benefit, but it isn't a requirement.

A tool, which can take an Ada package specification, and generate a command-line driver for calling the procedures declared in the package. Which of the procedures is called is controlled by the names of the arguments passed to the driver program. The presentation will cover: how to use the tool; and some details of how the tool works - using the Ada Semantic Interface Standard (ASIS).

Contract-based programming is a software development technique, which is used to find programming errors earlier in the development process. "Contract" refers to formal declarations of how types and subprograms ("functions and methods" if you aren't an Ada programmer already) behave. In the strictest form, the contracts are checked as a part of the compilation process, and only a program which can be proven to conform with the contracts will compile. In a less strict form, it is more similar to "preventive debugging", where the contracts are inserted as run-time checks, which makes it more likely to identify errors during testing.

Ada provides a quite extensive support for contract-based programming. The checks are specified as a mix of compile-time checks, obligatory run-time checks, and optional run-time checks. In addition to that, SPARK defines a subset of Ada with full compile-time checks.

The presentation will introduce the Ada features related to contract-based programming, and provide suggestions for how to make use of the features in practice. It is organized in three main sections: type/object invariants; pre- and postconditions for operations; making the contracts for entire packages consistent. If there is time, the presentation will close with a live test of the guidelines on an example problem selected by the audience.

The intended audience is anybody with enough programming experience to know concepts like types, encapsulation and packages. Having seen source text in Pascal-like programming languages will be a benefit.

A tutorial on how to use the Ada 2012 features for specifying detailed, checked contracts for types and subprograms -- "classes, functions, and methods" if you aren't an Ada programmer already.

Contracts document constraints on how types and subprograms behave, but unlike comments they are checked -- either by when the program is compiled or on-the-fly as the program is running.

Ada 2012 contract aspects will be presented together with a set of guidelines for using contract aspects consistently. The tutorial will conclude with a live test of the guidelines on some example source text.

Programming Arduinos made even easier (and more reliable).

An introduction to programming Arduinos and compatible ATMEL based devices in Ada. The talk will give a short explanation of how you can set up an Ada development environment for Arduinos, followed by some real-life code and devices, demonstrating some of the elegance you can get from using Ada for programming embedded systems.

Using Ada to provide business logic, and glue existing applications together.

The children's game universe "Crimeville" from the game developers Art of Crime challenges the players to solve detective riddles cooperatively. In the on-line version of the game this means that the players in each session of the game can chat with each other. To help the children write better - and to limit them being naughty - the chat is going through a language server written in Ada. The language server uses pre-existing Open Source spell-checking components glued together with application logic written in Ada. The application is a nice example of a small network server and of using parts of the POSIX Ada API (FLORIST). The presentation will cover the requirements from Art of Crime in broad terms, describe how this was achieved using publicly available Open Source components, and how using Ada helped convincing the customer that the system actually does its job.