| address: | Informatik 1, Technische Universität Dortmund |
|
|
D-44227 Dortmund, Germany |
| phone: | +49 231 755 5108 |
| room: | 2.023, Otto-Hahn-Str. 12 |
| secretary: | +49 231 755 6223 |
| fax: | +49 231 755 6555 |
|
|
peter.padawitz@udo.edu |
A Formal Methods Presenter
and Animator
Having started as the successor of Expander (see below), Expander2 is a multi-purpose workbench for interactive logical inference, constraint solving, data flow analysis, rewriting logic and related procedures building up proofs or computation sequences. Moreover, several interpreters translate expressions into tailor-made two-dimensional representations that range from trees and term graphs to tables, fractals and other turtle-system-generated pictures.
Expander2 is equipped with a GUI that permits the user to interact with the system at three levels of decreasing control over proofs and computations. At the first level, rules like induction and coinduction are applied locally and step by step. At the second level, goals are rewritten or narrowed, i.e. axioms are applied exhaustively and iteratively. At the third level, built-in rules (some of them execute Haskell programs) simplify, i.e. (partially) evaluate terms and formulas, and thus hide routine steps of a proof or computation.
Expander2 has been written in O'Haskell, an extension of Haskell with object-oriented features for reactive programming and a typed interface to Tcl/Tk. Besides a comfortable GUI the design goals of Expander2 were to integrate testing, proving and visualizing deductive methods, admit several degrees of interaction and keep the system open for extensions or adaptations of individual components to changing demands.
Proofs and computations performed with Expander2 follow the rules and the semantics of swinging types. Swinging types combine constructor-based visible types with state-based hidden ones and have unique Herbrand models that interpret relations as the least or greatest solutions of their axioms.
Expander: A System for Testing
and Verifying Functional-Logic Programs Expander is a proof and test environment for algebraic data type specifications and functional-logic programs. Program design, test and verification are supported by tailor-made deduction rules for proving Gentzen clauses, which are the most frequently used formulas for expressing requirements and queries to data types. Inductive proofs are built up from simplification, subsumption, resolution, rewriting and narrowing steps in a natural way that permits interaction on various levels. The core system is written in Standard ML. User interfaces are available for NeXTSTEP and X.
Painter and various further Haskell programs We present a number of new results on inductive theorem proving for design specifications based on Horn logic with equality. Induction is explicit here because induction orderings are supposed to be part of the specification. We show how the automatic support for program verification is enhanced if the specification satisfies a bunch of rewrite properties, summarized under the notion of canonicity. The enhancement is due to inference rules and corresponding strategies whose soundness is implied by the specification's canonicity. The second main result of the paper provides a method for proving canonicity by using the same rules, which are applied in proofs of conjectures about the specification and the functional-logic programs it contains.
Computing Rectangular
Dissections: Logical specifications provide an abstract level of programming where programs are given as axioms defining functions and predicates on constructor-based data types. Axiomatic function definitions are transformed into functional programs, predicate definitions are compiled into logic programs. If functions are to be implemented as logic programs, they must be flattened into predicates. In this paper, we exemplify the inverse translation: predicates used as multi-valued, nondeterministic, functions are compiled into stream-generating functions, which enumerate multiple values. Generate-and-test algorithms, usually implemented as logic programs, can be realized in this way as functional programs. Our case study deals with a configuration problem. Two nondeterministic algorithms that compute rectangular dissections are specified in the functional-logic language of Expander, flattened into Prolog programs, and, alternatively, translated into ML programs, which produce streams of dissections. Besides the compilation of predicates into stream functions the case study illustrates the use of polymorphic types and higher-order functions for accomplishing well-structured and reusable software.
Building Shelf Systems:
Unchecked version! Chapter 12 of Einführung ins funktionale Programmieren contains a revised version.
We present a generic functional program for loading (two-dimensional) containers with arbitrary objects, filling shelves with items of different kinds and - last not least - designing complete shelf systems. This piece of software and its development is a case study in functional programming for solving hierarchical configuration problems. Such problems require tailor-made, but nevertheless abstract and generic data models and algorithms. We claim that these are more directly realizable in a functional language than in a classical imperative language. Polymorphism, module abstraction, semantically well-founded exception handling and the problem-oriented option for static data, "lazy" structures (streams) or dynamic objects are the main concepts of functional programming we are going to use and explain in the context of our case study.
