Research on Theoretical Aspects of Evolutionary Software

计算环境正在从“顺序”向“并行和/或分布式”发展，应用正在向在效率、时间、规格和验证等方面要求更精细的需求和要求发展。在此背景下，本项目对可进化计算机软件的模型及其理论方面进行了研究。T. Ito为函数式程序提供了一种将顺序程序转换为并行程序的良好的并行化框架，使所得到的并行程序比原来的顺序程序运行得更快。在互联网环境下发展的分布式程序的验证和规范是一个重要的问题。M. Hagiya提出了一个关于验证方法的验证以及如何演进验证条件的有趣想法。Yonezaki研究了如何使用时间逻辑和线性逻辑来指定和验证实时反应系统，并给出了时间结构的各种基本形式性质。T. Ida研究了函数式逻辑程序的一些基本特性，并应用可执行规范，实现了一个分布式系统下的函数式逻辑程序设计系统。术语重写系统（TRS）为各种结构的执行提供了细粒度的操作机制，包括可演化的程序和机制。Sakabe给出了一个自适应trs模型。Y. Toyama给出了trs的分析和合成方法，以及一个强有力的证明trs终止的程序。此外，还完成了一些关于线性逻辑及其扩展的有趣工作，包括1)引入时间线性逻辑的建议（T. Ito）， 2)具有局域性和时间性的线性逻辑语言（K. Kobayashi）， 3)将线性逻辑和并发TRSs结合起来用于实时系统的规范和验证的建议（M. Okada）， 4)线性逻辑编程语言的高效编译器（N. Tamura）。此外，K. Kobayashi提出了一种保证死锁自由的分布式系统的类型系统，S. Nishizaki提出了一种环境演算，它是ML的扩展，将环境合并到ML中

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