Formal Specification of Program Module Interfaces

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

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.