Benutzer: Gast  Login
Originaltitel:
Analyzing Java in Isabelle/HOL 
Originaluntertitel:
Formalization, Type Safety and Hoare Logic 
Übersetzter Titel:
Analyse von Java in Isabelle/HOL 
Übersetzter Untertitel:
Formalisierung, Typsicherheit und Hoare-Logik 
Jahr:
2001 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Nipkow, Tobias (Prof. Ph.D.) 
Gutachter:
Poetzsch-Heffter, Arnd (Prof. Dr.) 
Format:
Text 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Stichworte:
Java; formalization; operational semantics; type soundness; axiomatic semantics; Isabelle/HOL 
Schlagworte (SWD):
Java ; Isabelle ; HOL 
TU-Systematik:
DAT 362d 
Kurzfassung:
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...    »
 
Übersetzte Kurzfassung:
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...    »
 
Veröffentlichung:
Universitätsbibliothek der TU München 
Mündliche Prüfung:
09.02.2001 
Dateigröße:
1179370 bytes 
Seiten:
190 
Letzte Änderung:
02.04.2008