Formal Specification

A formal specification of a program is a mathematical formula that expresses a certain property that the given program is expected to satisfy.