Universität Bremen  
  FB 3  
  AG BKB > Publikationen > Suche > Deutsch
English
 

Suche nach Veröffentlichungen - Detailansicht

 
Art der Veröffentlichung: Sonstige
Autor: Dennis Walter
Titel: Monadic Dynamic Logic: Application and Implementation
Erscheinungsjahr: 2005
Art der Veröffentlichung: Master's Thesis (Diplomarbeit)
Abstract / Kurzbeschreibung: The aim of this work is twofold: on the one hand, it constitutes the first extended application of the recently developed calculus of monadic dynamic logic and thus demonstrates how this calculus can be applied to serious verification tasks. To name two examples, the total correctness of a breadth-first search algorithm and of a pattern matching algorithm involving Java-like exception handling have been established. On the other hand, driven by the insight that due to the complexity even of relatively small software systems it is not feasible to carry out formal proofs about these manually, the calculus had to be implemented in some proof assistant tool. Furthermore, the formalisation within such a tool provides further evidence of the correctness of one’s inferences – provided one trusts in the correctness of the tool, of course. We chose the generic proof assistant (often termed ‘theorem prover’) Isabelle/HOL in which we could base our implementation on a stable and well developed formalisation of higher-order logic. Isabelle/HOL comes with tools for proving theorems outright (by means of a classical tableau reasoner) as well as a term rewriting system that allows for equational reasoning and functional programming. Tasks during this implementation included the definition of a syntax for monadic dynamic logic, proving the theorems needed as foundations for the logic, and working out theorems and setting up Isabelle’s automatic proof facilities to make life easier when applying the logic. The embedding into higher-order logic is a deep one in the sense that we define monadic logical connectives, as well as a predicate ` asserting the validity of monadic formulae. HOL formulae may, however, appear in monadic formulae thanks to existence of an insertion function Ret mapping HOL formulae into those of dynamic logic.
PDF Version: http://www.cs.chalmers.se/~denniswa/dipl-online.pdf
Schlagworte: monad dynamic logic HasCASL
Status: Other
Letzte Aktualisierung: 20. 06. 2006

 Zurück zum Suchergebnis
 
   
Autor: Automatisch generierte Seite
 
  AG BKB 
Zuletzt geändert am: 9. Mai 2023   impressum