U.S.-France Cooperative Research: Integrating a Theorem Prover and a Specification Environment

美法合作研究：集成定理证明器和规范环境

• 批准号: 9016780
• 负责人: John Guttag
• 金额: $ 1.27万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1991
• 资助国家: 美国
• 起止时间: 1991-04-01 至 1994-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9016780&HistoricalAwards=false
• 关键词: U.S.; France; Cooperative; Research; Integrating

This award will support collaborative research in software engineering between Drs. John Guttag and Stephen Garland, Massachusetts Institute of Technology and Drs. Michel Bidoit and Christine Choppy, Laboratoire de Recherche Informatique, University of Paris-Sud, France. The investigators propose a joint project that will first work on combining Assegigue, a specification environment under development at the University of Paris-Sud, and LP, a theorem proving system under development at MIT. They will then experiment with using the combined system to develop and reason about specifications. There is now widespread agreement that precise specifications can play a useful role in software development and maintenance. The most vexing problems in building systems deal with overall system organizations and the integration of components. Modularity is the key to controlling this, and specifications are essential for achieving modularity. Both the US and French research groups have adopted a style of specification that emphasizes brevity and clarity rather than executability. To make it possible to test specifications without executing or implementing them, both groups have developed techniques that enable specifiers to make claims about logical properties of specifications. However, whereas the French have centered their research around the technology needed to produce and manage large scale specifications, the MIT group has centered its research around the technology needed to check claims about logical properties of specification. By combining these two complementary research efforts, the investigators plan to produce a tool that can be used to develop, reason about and manage large-scale formal specifications of software.

该奖项将支持软件领域的合作研究 约翰·古塔格博士和斯蒂芬·加兰博士之间的工程学合作， 马萨诸塞州理工学院和Michel Bidoit博士 和克莉丝汀·肖比，信息研究中心， 法国南巴黎大学。调查人员提出了一个 联合项目将首先致力于将Assegigue（一个 正在开发的规范环境 和LP，一个定理证明系统 在MIT的发展。然后，他们将尝试使用 组合系统开发和推理规范。 现在人们普遍认为， 可以在软件开发和维护中发挥有用的作用。 建筑系统中最棘手的问题是 整体系统组织和组件集成。 模块化是控制这一点的关键， 是实现模块化的关键。 美国和 法国的研究小组采用了一种规范的风格， 强调简洁明了而不是可执行性。 为了能够测试规格而不执行 或实现它们，这两个小组都开发了技术， 使说明符能够声明逻辑属性 的规格。 然而，尽管法国人以 他们的研究围绕着生产所需的技术， 管理大规模的规范，麻省理工学院的小组已经集中在 它的研究围绕着核查索赔所需的技术， 关于规范的逻辑属性。 通过组合这些 两个互补的研究工作，研究人员计划， 产生一种工具，可以用来开发，推理， 管理大规模软件的形式化规范。