Algebraic techniques have been very successful in specifying and reasoning about data types. Hidden algebra extends these techniques to systems with state. The hidden algebra approach takes as basic the notion of behavioural abstraction: this means that specifications characterise how objects (and systems) behave. Models of hidden specifications can be thought of as abstract machines that implement the specified behaviour. Behavioural satisfaction of equations means that the left and right sides of the equations denote states that cannot be distinguished by their outputs. In this sense, hidden algebra is an algebraic treatment of abstract automata. * visible sorts are used for data values, while * hidden sorts are used for states. In a sense, these two uses of sorts are dual: induction can be used to establish properties of data types, whereas coinduction establishes properties of objects with state.