Type Inference of Object-Oriented Programs with Exceptions Based on Term Rewriting

基于术语重写的面向对象程序异常类型推断

• 批准号: 16300005
• 负责人: SAKABE Toshiki
• 金额: $ 3.86万
• 依托单位: Nagoya University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2004
• 资助国家: 日本
• 起止时间: 2004 至 2007
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-16300005/
• 关键词: Object-Oriented Program; Exception Handling; Secrecy; Type Inference; Term Rewriting System; 通信エラー; 逆計算

The purpose of this research is to develop static verification methods for safeness of programs by applying rich results obtained so far on term rewriting systems, and also to create new research topics of term rewriting systems.There are three main topics of this research : safeness of programs, termination of term rewriting systems and program transformations. (1) As for safeness of programs, we have developed a type system for verifying secrecy of object-oriented programs with exceptions, a type system for checking communication errors in programs of Join JAVA, which is a JAVA combined with Join Calculus, and also methods for verifying safeness of programs of Spi Calculus and Petri Net. (2) For termination of term rewriting systems, a result on decidability of termination has been obtained. Sufficient conditions for termination of higher order term rewriting systems have been obtained by extending the dependency pair method. (3) In the research of program transformation, an inversion procedure for term rewriting systems has been developed. Being triggered by the work on program safeness we have given a sufficient condition for termination of a procedure transforming systems of eqations to systems of rewriting rules, where this transformation is used in the secrecy verification procedure for the applied pi calculus.

这项研究的目的是通过应用迄今为止在术语重写系统中获得的丰富成果来开发静态验证方法，以使计划的安全性，并创建了术语重写系统的新研究主题。这项研究的三个主要主题：计划的安全性，终止术语重写系统和程序转换。 （1）关于程序的安全性，我们开发了一种类型系统，用于验证以对象为导向的程序的保密性，但有例外，一种用于检查Join Java程序中通信错误的类型系统，Jon Java是一种与Join Cyculus结合使用的Java，以及用于验证Spi Calculus和Petri Net程序的方法。 （2）对于终止术语重写系统，已经获得了终止可决定性的结果。通过扩展依赖关系对方法，已经获得了足够的终止高阶术语重写系统的条件。 （3）在计划转换的研究中，已经开发了针对术语重写系统的反转程序。在程序安全性上的工作触发的是，我们给出了足够的条件，可以终止将架子的系统转换为重写规则系统的过程，在这种情况下，在应用PI计算的保密验证过程中使用了此转换。

项目成果

Higher-Order Knuth-Bendix Procedure and its Applications

高阶 Knuth-Bendix 过程及其应用

• 发表时间: 2004
• 期刊: LA-Symposium 2004(Summer)
• 作者: K.Kusakari;Y.Chiba
• 通讯作者: Y.Chiba

Enhancing Dependency Pair Method by Strong Computability in Simply-Typed Term Rewriting

通过简单类型术语重写中的强可计算性增强依赖对方法

• 发表时间: 2007
• 期刊: Applicable Algebra in Engineering, Communica-tion and Computing 18
• 作者: Keiichirou Kusakari;Masahiko Sakai
• 通讯作者: Masahiko Sakai

Convergent Term Rewriting Systems for Inverse Computation of Injec-tive Fhnctions

单射函数逆计算的收敛项重写系统

• 发表时间: 2007
• 期刊: Proc. of the 9th International Workshop on Ter-mination
• 作者: Naoki Nishida;Masahiko Sakai;and Terutoshi Kato
• 通讯作者: and Terutoshi Kato

Usable Rules and Labeling Product-Typed Terms for De-pendency Pair Method in Simply-Typed Term Rewriting Systems

简单类型术语重写系统中依赖对方法的可用规则和标签产品类型术语

• 发表时间: 2007
• 期刊: IEICE Transactions on Information and Systems Vol.J90-D, No.4(Refereed)
• 作者: Takahiro;Sakurai;Keiichirou;Kusakari;Masahiko;Sakai;Toshiki;Sakabe;Naoki;Nishida
• 通讯作者: Nishida

Static Dependency Pair Method for Proving Termination of Higher-Order Rewriting Systems

证明高阶重写系统终止的静态依赖对方法

• 发表时间: 2007
• 期刊: 電子情報通信学会技術研究報告(SS2007-61) 107
• 作者: Kiichirou Kusakari;Yasuo Iso-gai;Masahiko Sakai;Toshiki Sakabe Naoki Nishida
• 通讯作者: Toshiki Sakabe Naoki Nishida