Formal Specification of Program Module Interfaces

这项研究是基于落叶松家族的规格说明语言， 它支持规范的两层定义方法。 每个规范都有用两种语言编写的组件： 专为一种特定的编程语言和另一种通用的编程语言而设计 编程语言。 前者称为落叶松界面 语言，后者是落叶松共享语言。 以前的工作集中在共享语言上。 新的工作 将注意力转移到接口语言上;提供精确的语义 对于这些语言，使用它们来编写大量的接口， 规范，确定应该对这些规范应用什么检查。 规范，并开发执行这些检查的工具。

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.