The Larch Project develops aids for formal specifications.
Each Larch specification has two components: an interface
containing assertions about the
predicates written in LSL,
["The Larch Family of Specification Languages", J. Guttag et
al, IEEE Trans Soft Eng 2(5):24-365 (Sep 1985)].