Research and development projects

KORSO - Deduction oriented Development of Specifications

gleiche Information in Deutsch

Dr. Radu Grosu
Dr. Rudi Hettler
Dr. Dieter Nazareth
Dr. Franz Regensburger
Dipl.-Inform. Oscar Slotosch

Project part of the BMFT - compound project KORSO, "Korrekte Software". See KORSO-Bremen and KORSO-Berlin for other home pages of other project parts.

Methodical programming requires an expressive language. The language SPECTRUM was designed for the specification and development of software and hardware systems. SPECTRUM allows to describe systems in a property oriented way. The underlying logical calculus allows to handle the usual proof obligations in a deductive way. It is a calculus of natural deduction for a three-valued first order logic with induction principles. In difference to other algebraic languages SPECTRUM permits the use of partial functions, including non-strict ones, high-order functions and non-continuous functions. It uses a predicative polymorphism with type classes. Type classes are used to model overloading as well as many forms of parameterization. As an executable part of the language, SPECTRUM includes a functional language. Thus the language aims at the development of functional programs. The semantics of a specification is loose, given as the class of all models. In a stepwise refinement new properties are added to an existing specification. This leads to a restricted model class.

The language is especially designed for the modularization of large projects. Complex specifications can be hierarchically structured by combining specifications in combination with renaming and hiding. The language is powerful enough to express the implementation of specifications through more primitive specifications. With means of logical deduction it is possible to establish formal relationships between components of project documentation. The aim is to generate certain components automatically. To support the software development on a computer a collection of tools was designed. The ISABELLE theorem prover e.g. can be used to deduce theorems.

See also the description of project SPECTRUM which is related to the KORSO project.
Papers concerning SPECTRUM can be found here.
SPECTRUM is a project of our department for Programming Methods and Distributed Systems.
Oscar Slotosch , 19 Oct 1995