TU Darmstadt / ULB / tuprints

Verification of Second-Order Functional Programs

Aderhold, Markus Axel :
Verification of Second-Order Functional Programs.
Technische Universität Darmstadt
[Ph.D. Thesis], (2009)

[img]
Preview
PDF
Dissertation-Aderhold_final_sw.pdf
Available under Creative Commons Attribution Non-commercial No Derivatives.

Download (1521Kb) | Preview
Item Type: Ph.D. Thesis
Title: Verification of Second-Order Functional Programs
Language: English
Abstract:

Functional programming languages such as Haskell or ML allow the programmer to implement and to use higher-order procedures. A higher-order procedure gets a function as argument and applies this function to some values. For instance, procedure 'map' applies a function to all elements of a list and returns the list of the result values. Verifying that a higher-order program satisfies a certain property is particularly challenging, because it involves reasoning about indirect function calls; for instance, a call 'map(f, l)' directly calls procedure 'map' and indirectly calls function 'f' if list 'l' is non-empty. Using a higher-order procedure 'g', a procedure 'f' can be defined by higher-order recursion; i. e., procedure 'f' (directly) calls 'g' and passes itself as an argument to 'g', which leads to indirect recursive calls. These indirect recursive calls make reasoning about higher-order programs difficult. In this thesis we show how the verification of second-order functional programs can be supported by semi-automated theorem provers. 'Second-order' means that a procedure such as 'map' may only be applied to a first-order function, not to a higher-order function. This suffices for most examples that occur in practice and has advantages concerning the semantics of programs. Our goal is to verify the total correctness of programs. This requires a proof that the program terminates and that the result of the computation satisfies a user-defined property. Consequently, we investigate two main problems: termination analysis and inductive theorem proving. The general contribution of this thesis is the automated analysis of the dynamic call structure in second-order programs (introduced by indirect function calls). Specifically, we describe a technique that automatically analyzes and proves termination of many procedures that occur in practice and a technique that automatically synthesizes induction axioms that are suitable to prove properties of these procedures by induction. Finally, we show how the proof of the base and step cases can be supported by an automated theorem prover. The techniques have been implemented in the verification tool VeriFun. Several case studies confirm that they work well in practice and provide a significantly higher degree of automation than other inductive theorem provers.

Alternative Abstract:
Alternative AbstractLanguage
Funktionale Programmiersprachen wie etwa Haskell oder ML erlauben dem Programmierer, Prozeduren höherer Ordnung zu implementieren und zu verwenden. Eine Prozedur höherer Ordnung bekommt eine Funktion als Argument und wendet diese Funktion auf gewisse Werte an. Zum Beispiel wendet die Prozedur "map" eine Funktion auf alle Elemente einer Liste an und gibt die Liste der Ergebniswerte zurück. Der Nachweis, dass ein Programm höherer Ordnung eine gewisse Eigenschaft erfüllt, birgt besondere Herausforderungen, weil insbesondere auch indirekte Funktionsaufrufe zu betrachten sind: Der Aufruf "map(f, l)" enthält beispielsweise einen direkten Aufruf der Prozedur "map" und indirekte Aufrufe der Funktion "f", falls die Liste "l" nicht leer ist. Unter Verwendung einer Prozedur "g" höherer Ordnung kann eine Prozedur "f" durch so genannte Rekursion höherer Ordnung definiert werden. Dies bedeutet, dass die Prozedur "f" (direkt) die Prozedur "g" aufruft und sich selbst als Argument an "g" übergibt, was zu indirekten rekursiven Aufrufen führt. Diese indirekten rekursiven Aufrufe erschweren die Beweisführung über Programme höherer Ordnung. In dieser Dissertation zeigen wir, wie die Verifikation funktionaler Programme zweiter Ordnung durch halb-automatische Theorembeweiser unterstützt werden kann. Der Fokus auf Programme zweiter Ordnung bedeutet, dass eine Prozedur wie etwa "map" nur auf Funktionen erster Ordnung angewendet werden darf, nicht auf Funktionen höherer Ordnung. Dies genügt für die meisten in der Praxis auftretenden Beispiele und bietet Vorteile hinsichtlich der Semantik von Programmen. Unser Ziel ist der Nachweis der totalen Korrektheit von Programmen. Dies erfordert einen Beweis, dass das Programm terminiert und dass das Ergebnis der Berechnung eine vom Benutzer spezifizierte Eigenschaft erfüllt. Dementsprechend untersuchen wir zwei Hauptprobleme: Terminierungsanalyse und Theorembeweisen durch Induktion. Der allgemeine Beitrag dieser Dissertation ist die automatisierte Analyse der dynamischen Aufrufstruktur von Programmen zweiter Ordnung (verursacht durch indirekte Funktionsaufrufe). Insbesondere beschreiben wir eine Technik, die die Terminierung von zahlreichen in der Praxis auftretenden Prozeduren analysiert und beweist, sowie eine Technik, die automatisch Induktionsaxiome erzeugt, die zum Nachweis von Eigenschaften dieser Prozeduren mittels Induktion geeignet sind. Schließlich zeigen wir, wie die Beweise der Basis- und Schrittfälle durch einen automatisierten Theorembeweiser unterstützt werden können. Die vorgestellten Techniken wurden im Verifikationswerkzeug VeriFun implementiert. Mehrere Fallstudien zeigen, dass sich die Techniken in der Praxis bewähren und einen deutlich höheren Automatisierungsgrad bieten als andere induktive Theorembeweiser.German
Uncontrolled Keywords: verification, functional programs, second-order, higher-order, deduction, induction, automated theorem proving, termination, correctness, automated reasoning
Alternative keywords:
Alternative keywordsLanguage
verification, functional programs, second-order, higher-order, deduction, induction, automated theorem proving, termination, correctness, automated reasoningEnglish
Classification DDC: 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
Divisions: Fachbereich Informatik
Fachbereich Informatik > Programmiermethodik
Date Deposited: 03 Sep 2009 08:24
Last Modified: 07 Dec 2012 11:55
URN: urn:nbn:de:tuda-tuprints-18652
License: Creative Commons: Attribution-Noncommercial-No Derivative Works 3.0
Referees: Walther, Prof. Dr. Christoph and Mantel, Prof. Dr. Heiko
Refereed: 14 July 2009
URI: http://tuprints.ulb.tu-darmstadt.de/id/eprint/1865
Export:

Actions (login required)

View Item View Item