Stepwise software developement : Combining axiomatic and algorithmic approaches in algebraic specifications

Abstract

Much of the software development activity can be carried out using formal specifications that have a precise and well defined semantics, making it possible to formally verify the correctness of the development steps. In order to support this claim we present an algebraic specification method that provides both axiomatic and algorithmic techniques and illustrate it by working through an example development. Our method is realized in the specification development language ASPIK, which is a core component of an integrated software development and verification system. The semantics of ASPIK is based on the new notion of canonical term functor which generalizes the notion of canonical term algebra, and we show how this notion allows a uniform integration of axiomatic and algorithmic approaches by using the concept of algorithmic constraints.