[VAK 03-604.03] Formal Methods of Software Development I
Till Mossakowski
Lutz Schröder
K 4 SWS
Mon 13:00 - 15:00 MZH 7230,
Wed 15:00 - 17:00 MZH 7250
First lecture Wednesday, October 20th, 2004
In modern software development, applications that require, for safety reasons, a reliable, permanent and correct functioning of the product play a role of increasing importance. This course is about methods of precise specification of correctness requirements and about how these are guaranteed to hold during the whole development process. The course will be based on formal specification languages, testing tools and semi-automatic theorem provers. The implementation language will be Haskell.
Overview of the course
- Testing with user-defined test cases: HUnit (you will also need a Haskell Compiler)
Call ghci with the option -i<path>/HUnit (no space between -i and the path).
Call hugs with the option -S.lhs - Testing with automated test-case generation: QuickCheck
- Testing monadic programs
- Programatica's P-logic Sample P-logic proof Installation of programatica
- Isabelle/HOL: verification of simple functional programs
- Isabelle/HOLCF: verification of general functional programs
- From P-logic to HOLCF
Slides: lect1 lect2 lect3 lect4 lect5 lect6
Isabelle Slides: Lecture 1; the meta-logic; primitive recursion; unification and resolution; simplification
Isabelle Examples: Script for demo application of a meta-rule (in classical Isabelle -- type isabelle HOL)
Isabelle Problems: sheet 1; deliverable exercise
Haskell examples: QuickCheck examples Queues State Monad
Exercises: ex1 sample test cases ex2 sample programs ex3 sample solution ex4 (Isabelle exercises see above)
Related lecture: Advanced techniques of functional programming (Wed 17-19h, MZH 8090)
Literature
- The Haskell Bookshelf
- Simon Thompson. Haskell: The Craft of Functional Programming Second Edition, Addison-Wesley, 507 pages, paperback, 1999. ISBN 0-201-34275-8.
- Richard B. Kieburtz. P-logic: Property Verification for Haskell Programs
- Thomas Hallgren. Haskell Tools from the Programatica Project - Demo Abstract
- Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic LNCS 2283, Springer Verlag, 2004.
- Franz Regensburger. HOLCF: Higher Order Logic of Computable Functions LNCS 971, 293--?, Springer Verlag, 1995
- Franz Regensburger. HOLCF: Eine konservative Erweiterung von HOL um LCF. Dissertation, TU München, 1994.