KIT | KIT-Bibliothek | Impressum | Datenschutz
Open Access Logo
§
Volltext
DOI: 10.5445/IR/1000012399

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.


Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Hochschulschrift
Jahr 2009
Sprache Englisch
Identifikator URN: urn:nbn:de:swb:90-123994
KITopen-ID: 1000012399
Verlag Karlsruhe
Abschlussart Abschlussarbeit - Diplom
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page