User: Guest  Login
Original title:
Analyzing Java in Isabelle/HOL
Original subtitle:
Formalization, Type Safety and Hoare Logic
Translated title:
Analyse von Java in Isabelle/HOL
Translated subtitle:
Formalisierung, Typsicherheit und Hoare-Logik
Author:
von Oheimb, David
Year:
2001
Document type:
Dissertation
Institution:
Fakultät für Informatik
Advisor:
Nipkow, Tobias (Prof. Ph.D.)
Referee:
Poetzsch-Heffter, Arnd (Prof. Dr.)
Format:
Text
Language:
en
Subject group:
DAT Datenverarbeitung, Informatik
Keywords:
Java; formalization; operational semantics; type soundness; axiomatic semantics; Isabelle/HOL
Controlled terms:
Java ; Isabelle ; HOL
TUM classification:
DAT 362d
Abstract:
This thesis deals with machine-checking a large sublanguage of sequential Java, covering nearly all features, in particular the object-oriented ones. It shows that embedding such a language in a theorem prover and deducing practically important properties is meanwhile possible and explains in detail how this can be achieved. We formalize the abstract syntax, and the static semantics including the type system and well-formedness conditions, as well as an operational (evaluation) semantics of the...    »
Translated abstract:
Diese Dissertation behandelt die maschinelle Analyse des (fast vollständigen) sequentiellen Teils der objektorientierten Programmiersprache Java. Wir zeigen, dass die Einbettung einer solchen Sprache in einen Theorembeweiser, in diesem Fall Isabelle/HOL, und der Beweis wichtiger metatheoretischer Eigenschaften inzwischen gut möglich ist. Dazu beschreiben wir detailliert die Formalisierung mit Abstrakter Syntax, Typsystem und der Operationellen Semantik sowie ein Anwendungsbeispiel, geben einen B...    »
Publication :
Universitätsbibliothek der TU München
Date of submission:
30.11.2000
Oral examination:
09.02.2001
File size:
1179370 bytes
Pages:
190
Last change:
02.04.2008
 BibTeX