Home | english  | Impressum | Sitemap | KIT

Formal Semantics for the Java Modeling Language

Formal Semantics for the Java Modeling Language
Typ:Diplomarbeit
Datum:2009
Betreuer:

Prof. P. H. Schmitt
Mattias Ulbrich
Benjamin Weiß

Bearbeiter:

Daniel Bruns

Links:PDF

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 ofizielle 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 ab-
gebildet werden, um eine nahezu vollständige Übersicht der Spezifikationen für sequentielle Java-Programme zu entwickeln.

BibTeX

@MastersThesis{bruns09,
  author =      "Daniel Bruns",
  title =       "Formal Semantics for the {J}ava {M}odeling {L}anguage",
  year =        2009,
  month =       jun,
  school =      "Universit{\"{a}}t {K}arlsruhe",
  type =        "Diploma thesis",
}