KIT | KIT-Bibliothek | Impressum | Datenschutz

Formal Semantics for the Java Modeling Language

Bruns, Daniel

Abstract:
Diese Arbeit beschäftigt sich mit der Semantik der Java Modeling Language (JML). JML is eine weitverbreitete Spezifikationssprache, die speziell auf Java zugeschnitten ist und sowohl zur statischen als auch zur Laufzeitanalyse von Programmen verwandt wird. Bislang beschränkt sich die offizielle Spezifikation von JML auf eine weitgehend verbale Definition der Semantik, die zudem teilweise unvollständig oder widersprüchlich ist. Daraus erwächst unter anderem, dass die verschiedenen Software-Werkzeuge, die JML implementieren, Sprachelemente der JML unterschiedlich auslegen. Bisherige Arbeiten zur formalen Semantik basieren auf Logiken höherer Ordnung oder dynamischen Logiken. In dieser Arbeit wird ein Ansatz vorgestellt, der nur auf elementaren mathematischen Konzepten wie Mengen, Funktionen und Prädikatenlogik erster Ordnung beruht. In dieser Arbeit wird eine simple Abstraktion einer Maschine vorgestellt, auf der der semantische Unterbau basiert, auf welchen Ausdrücke und Spezifikationen von JML abgebildet werden, um eine nahezu vollständige Übersicht der Spezifikationen für sequentielle Java-Programme zu entwickeln.

Open Access Logo


Volltext §
DOI: 10.5445/IR/1000012399
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Hochschulschrift
Publikationsjahr 2009
Sprache Englisch
Identifikator urn:nbn:de:swb:90-123994
KITopen-ID: 1000012399
Verlag Universität Karlsruhe (TH)
Art der Arbeit Abschlussarbeit - Diplom
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page