TY  - UNPD
A1  - Sabel, David
A1  - Schmidt-Schauß, Manfred
T1  - Reconstruction of a logic for inductive proofs of properties of functional programs
T2  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 39
N2  - 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.
T3  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 39 [v.2] 
KW  - Formale Semantik
KW  - Logik
KW  - Verifikation
Y1  - 2010
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34437
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30:3-344375
UR  - http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank-39_v2.pdf
IS  - Version: 31 März 2010
EP  - 41
PB  - Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik
CY  - Frankfurt am Main
ER  -