REASONING ABOUT STATE BASED SYSTEMS USING COINDUCTION AND CORECURSION

State based systems abound in Computer Science. Automata, transition systems, streams, and object oriented programs are just a few examples. Universal coalgebra is a mathematical theory for a unified treatment of all such systems. It provides a general perspective which, aside from the above mentioned examples, permits to view topological spaces as state based systems. In specifications and descriptions, explicit references to internal states should be avoided. The mathematical tools needed are coinduction and corecursion. We give several examples and applications of coalgebras in computer science and mathematics, and we show how to specify methods corecursively and how to prove system properties coinductively.