3 Getting Started

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.