Formal Specification of Program Module Interfaces

程序模块接口的形式规范

• 批准号: 8910848
• 负责人: John Guttag
• 金额: $ 21.31万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1989
• 资助国家: 美国
• 起止时间: 1989-07-15 至 1991-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=8910848&HistoricalAwards=false
• 关键词: Formal; Specification; 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.

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