Reconstruction of a logic for inductive proofs of properties of functional programs
- The interactive verification system VeriFun is based on a polymorphic call-by-value functional language and on a first-order logic with initial model semantics w.r.t. constructors. It is designed to perform automatic induction proofs and can also deal with partial functions. This paper provides a reconstruction of the corresponding logic and semantics using the standard treatment of undefinedness which adapts and improves the VeriFun-logic by allowing reasoning on nonterminating expressions and functions. Equality of expressions is defined as contextual equivalence based on observing termination in all closing contexts. The reconstruction shows that several restrictions of the VeriFun framework can easily be removed, by natural generalizations: mutual recursive functions, abstractions in the data values, and formulas with arbitrary quantifier prefix can be formulated. The main results of this paper are: an extended set of deduction rules usable in VeriFun under the adapted semantics is proved to be correct, i.e. they respect the observational equivalence in all extensions of a program. We also show that certain classes of theorems are conservative under extensions, like universally quantified equations. Also other special classes of theorems are analyzed for conservativity.
Author: | David SabelORCiDGND, Manfred Schmidt-SchaußORCiDGND |
---|---|
URN: | urn:nbn:de:hebis:30:3-344375 |
URL: | http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank-39_v2.pdf |
Parent Title (English): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 39 |
Series (Serial Number): | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (39 [v.2]) |
Publisher: | Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik |
Place of publication: | Frankfurt am Main |
Document Type: | Working Paper |
Language: | English |
Date of Publication (online): | 2010/03/31 |
Date of first Publication: | 2010/03/31 |
Publishing Institution: | Universitätsbibliothek Johann Christian Senckenberg |
Release Date: | 2014/07/08 |
GND Keyword: | Formale Semantik; Logik; Verifikation |
Issue: | Version: 31 März 2010 |
Page Number: | 41 |
Last Page: | 41 |
HeBIS-PPN: | 344379809 |
Institutes: | Informatik und Mathematik / Informatik |
Dewey Decimal Classification: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
Sammlungen: | Universitätspublikationen |
Licence (German): | Deutsches Urheberrecht |