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 
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 
Oral examination:
09.02.2001 
File size:
1179370 bytes 
Pages:
190 
Last change:
02.04.2008