#
Research and development projects

##
KORSO - Deduction oriented Development of Specifications

* gleiche Information in Deutsch*

**Contact:**

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