Springer
CD-ROM OverviewTable of ContentsSearch

3  Getting Started

Michel Bidoit1 and Peter D. Mosses2

1 Laboratoire Spécification et Vérification, CNRS UMR 8643
École Normale Supérieure de Cachan
61, Avenue du Président Wilson, 94235 Cachan Cedex, France
bidoit@lsv.ens-cachan.fr

2 University of Aarhus, BRICS and Department of Computer Science
Aabogade 34, 8200 Aarhus N, Denmark
pdmosses@brics.dk

Abstract. Simple specifications may be written in CASL essentially as in many other algebraic specification languages.

The simplest kind of algebraic specification is when each specified operation is to be interpreted as an ordinary total mathematical function: it takes values of particular types as arguments, and always returns a well-defined value. Total functions correspond to software whose execution always terminates normally. The types of values are named by simple symbols called sorts.

In practice, a realistic software specification involves partial as well as total functions. However, it may well be formed from simpler specifications, some of which involve only total functions. This chapter explains how to express such simple specifications in CASL, illustrating various features of the language.

The simple specifications discussed in this chapter can also be expressed in many previous specification languages; it is usually straightforward to reformulate them in CASL. Readers who know other specification languages will probably recognize some familiar examples among the illustrations given in this chapter.

LNCS 2900, pp. 23 - 45

Full article in PDF


lncs@springer.de
© Springer-Verlag Berlin Heidelberg 2004