Johannes Kliemann

Gneiss is an abstraction layer for component based environments that aims to provide a foundation for formally provable components. It enables the creation of platform independent, asynchronous components in SPARK and provides function contracts that allow to prove the correct interaction with the underlying platform.

Last year I presented Cappulada, a C++ binding generator for Ada that intended to overcome the shortcomings of existing solutions and to provide usable bindings even for complex C++ code.

This year I want to show our conclusions on why automatic bindings between C++ and Ada are hard (if not impossible) and where existing solutions (including our own) fail.

Writing Ada bindings for C and especially for C++ is a tedious but not necessarily sophisticated task. There are several approaches to both C and C++ but many of them lack desired language features, generate non-compilable code or are project specific.

With Cappulada (a coinage of coupling, CPP and Ada made pronounceable) we try a more general approach that aims to support complex language features such as templates or inheritance while providing a semantically appropriate mapping of object structures and types. The talk will also cover which features can be mapped and what is not feasible or possible.

An introduction on SPARK, a programming language specifically designed for high reliability and used in safety critical areas such as avionics or railway signaling or in high security applications such as the Muen micro kernel or the WooKey, a secure USB mass storage device.