language, specification An algebraic specificationlanguage by David Aspinall of the University of Edinburgh.

ASL+ has rules for proving the satisfaction of specifications.

It can also be viewed as a type theory with subtyping,

featuring contravariant refinement for Pi-abstracted

specifications and a notion of stratified equality for

higher-order objects.