Eines der schwierigsten Softwareentwicklungsproble ist das Finden von Programmierfehlern. Aus diesem Grund ermuntern moderne Softwareentwicklungsmethodologien Programmierer dazu, prüfbare Aussagen (assertions) in ihren Programmen unterzubringen. Diese Aussagen drücken Annahmen aus, die der Programmierer über das Verhalten des Programmes hat; wenn sie zur Laufzeit überprüft werden, ist es somit leicht möglich, irrige Annahmen und damit oft Programmierfehler aufzudecken. Existierende Sprachen für solche prüfbaren Aussagen, wie man sie in C und Java findet, haben allerdings nur beschränkte Ausdrucksfähigkeit.
Dieser Vortrag stellt DeAL vor, eine ausdruckskräftige Sprache für prüfbare Aussagen in Java. DeAL erweitert den traditionellen Sprachschatz für solche Aussagen um Relationen, die die Struktur des Ablagespeichers (heap) beschreiben. Diese Spracherweiterungen erlauben es, zuvor nicht überprüfbare Eigenschaften auszudrücken, wie zum Beispiel globale Invarianten oder Eignerbeziehungen (ownership properties).
Das Design von DeAL ermöglicht es, das alle solchen Eigenschaften in einer einzigen Iteration über den Ablagespeicher überprüft werden können. DeAL kann somit in die automatischen Speicherverwaltung der Sprache integriert werden; wie unsere Experimente zeigen, erlaubt dies die Überprüfung von DeAL-Aussagen mit sehr geringen Laufzeitkosten.