A specification for software expressed in a (mathematically) formal language such that the specification is completely independent of, and does not imply, any design and implementation method and languages. It does not normally express the constraints that the final software must satisfy. See also formal specification.