| ## 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