WSL is a "Wide Spectrum Language" which includes both low-level programming constructs and high-level abstract specifications within a single language. Such a language forms an ideal tool for developing methods for formal program development, and also for formal reverse engineering, because the proof that a program correctly implements a specification, or that a specification correctly captures the behaviour of a program, can be achieved by means of semantic-preserving transformations in the language.

For nearly twenty years we have been developing this wide spectrum language, in parallel with the development of a transformation theory and proof methods, together with methods for program development and inverse engineering.