The Tau language is a language extension of other classical logics (the “base logics”) intended to be a logic whose formulas denote software specifications.