Research on Theoretical Aspects of Evolutionary Software

进化软件理论方面的研究

• 批准号: 09245102
• 负责人: ITO Takayasu
• 金额: $ 26.24万
• 依托单位: Tohoku University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research on Priority Areas
• 财政年份: 1997
• 资助国家: 日本
• 起止时间: 1997 至 1999
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-09245102/
• 关键词: evolutionary programming mechanism; sound parallelization; verification; reactive system; temporal logic; functional logic programming; term rewriting system; linear logic; 発展的ソフトウェア; ソフトウェア仕様記述; 論理・関数型プログラミング; 書換え型メタ計算モデル; 実時間論理; 検証系; 検証情報

Computational environments are evolving from "sequential" into "parallel and/or distributed", and applications are evolving into the ones that require finer demands and requirements in efficiency, time, specification and verification, etc.With this background models of evolvable computer software and their theoretical aspects were studied in this project.A sound parallelization framework of transforming a sequential program into a parallel program that the resultant parallel program runs faster than the original sequential one was given for functional programs by T. Ito.Verification and specification of distributed programs that evolve under internet environments are of important issues. M. Hagiya proposed an interesting idea of verification of verification methods and how to evolve verification conditions.N. Yonezaki studied bow to specify and verify real-time reactive systems, using temporal logics and linear logic, and he gave various basic formal properties on temporal structures. … More T. Ida studied some basic properties of functional logic programs with applications to executable specifications, and he implemented a functional logic programming system under a distributed system.Term rewriting systems (TRS) provide fine-grained operational mechanisms for executions of various structures, including evolvable programs and mechanisms.T. Sakabe gave a model of adaptive TRSs. Y. Toyama gave an analysis and synthesis method of TRSs, and a powerful procedure of proving termination of TRSs.Also, a number of interesting works on linear logic and its extensions were done, including 1) a proposal of introducing temporal linear logic (T. Ito), 2) a linear logic language with locality and temporality (K. Kobayashi), 3) a proposal of combining linear logic and concurrent TRSs for specification and verification of real-time systems (M. Okada), 4) an efficient compiler of linear logic programming language (N. Tamura). In addition, K. Kobayashi proposed a type system of distributed systems that guarantees deadlock-freedom, and S. Nishizaki proposed an environment calculus which is an extension of ML to incorporate environments into ML. Less

计算环境从“顺序”变成“平行和/或分布式”，并且应用程序不断发展为需要在效率，时间，时间，规格和验证等方面的最终需求和需求等。与该项目相比，该项目在该项目中的原始程序构成了一个顺序的程序，该计划的序列序列符合顺序的框架，该计划的序列序列序列的序列序列符合顺序的框架。对于T. Ito.的功能程序，在互联网环境下进化的分布式程序的验证和规范是重要的问题。 Hagiya M.提出了一个有趣的验证方法验证方法以及如何进化验证条件的想法。 Yonezaki使用临时逻辑和线性逻辑进行了研究，以指定和验证实时反应系统，并在临时结构上提供了各种基本的正式属性。 …更多的T. Ida研究了功能逻辑程序的一些基本属性，并使用可执行规格的应用程序进行了应用，他在分布式系统下实施了功能逻辑编程系统。Term重写系统（TRS）为执行各种结构的执行提供了精细的操作机制，包括可转换程序和机制。萨卡贝（Sakabe）给出了自适应TRS的模型。 Y. Toyama gave an analysis and synthesis method of TRSs, and a powerful procedure of providing termination of TRSs.Also, a number of interesting works on linear logic and its extensions were done, including 1) a proposal of introducing temporary linear logic (T. Ito), 2) a linear logic language with locality and temporary (K. Kobayashi), 3) a proposal of combining linear logic and concurrent TRSs用于实时系统的规范和验证（M. Okada），4）线性逻辑编程语言（N. Tamura）的有效编译器。此外，K。kobayashi提出了一种分布式系统的类型系统，可以保证僵持自由，而S. nishizaki提出了一种环境计算，该环境是ML的扩展，以将环境纳入ML。较少的

项目成果

Yasuaki Takebe and Masami Hagiya: "A User Interface for Controlling Term Rewriting Based on Computing-as-Editing Paradigm" User Interfaces for Theorem Provers UITP'97,INRIA Sophia-Antipolis. 93--100 (1997)

Yasuaki Takebe 和 Masami Hagiya：“基于计算即编辑范式的控制术语重写的用户界面”定理证明者 UITP97 的用户界面，INRIA Sophia-Antipolis。

Wei-Ngun CHIN, Masami HAGIYA: "A Bounds Inference Method for Vector-Based Memoization" International Conference on Functional Programming'97. 176--187 (1997)

Wei-Ngun CHIN、Masami HAGIYA：“基于向量的记忆化的界限推理方法”函数式编程国际会议97。

番原 睦、田村 直之: "線形論理型言語のJAVA言語による処理系の設計と実装"情報処理学会論文誌プログラミング. Vol.40, No.SIG10. 1-16 (1999)

Mutsumi Banhara、Naoyuki Tamura：“使用 JAVA 线性逻辑语言的处理系统的设计和实现”《日本信息处理协会编程学报》第 40 卷，第 1-16 期（1999 年）。

Takayasu Ito: "A Sound Parallelization Framework for Parallel Scheme Programming, Parallel and Distributed Computing for Symbolic and Irregular Applications"World Scientific. 2-39 (2000)

Takayasu Ito：“用于并行方案编程、符号和不规则应用程序的并行和分布式计算的健全并行化框架”世界科学。

Mitsuharu Yamamoto,Koichi Takahashi,Masami Hagiya,Shin-ya Nishizaki: "Formalization of Graph Search Algorithms and its Applications" Lecture Notes in Computer Science,Springer-Verlag. Vol.1479. 479-496 (1998)

Mitsuharu Yamamoto、Koichi Takahashi、Masami Hagiya、Shin-ya Nishizaki：“图搜索算法的形式化及其应用”计算机科学讲义，Springer-Verlag。