me too is an executable formal specification language based on the mathematics of sets, tuples and functions. The me too tools are implemented in a purely functional subset of Common Lisp. I can recommend with absolutely no bias ;-) the excellent book

Alexander H and Jones V (1990)
Software Design and Prototyping using me too.
London: Prentice Hall International.