This research is based on the Larch family of specification languages, which support a two-tiered definitional approach to specification. Each specification has components written in two languages: one designed for a specific programming language and another common to all programming languages. The former are called Larch interface languages, and the latter the Larch Shared Language. Prior work has concentrated on the Shared Language. The new work shifts attention to interface languages; providing precise semantics for these languages, using them to write substantial interface specifications, determining what checking should be applied to these specifications, and developing tools for performing these checks.
