Research on Theoretical Aspects of Evolutionary Software

计算环境正在从“顺序”向“并行和/或分布式”发展，应用也向效率、时间、规格说明和验证等方面提出了更高的要求和要求。在这种背景下，本课题研究了可演化计算机软件的模型及其理论问题。伊藤忠雄为函数式程序给出了一个合理的并行化框架，将一个顺序程序转换成一个并行程序，得到的并行程序比原来的顺序程序运行得更快。M.Hagiya提出了一种有趣的验证方法和如何演化验证条件的思想。N.Yonezaki使用时序逻辑和线性逻辑来描述和验证实时反应系统，并给出了关于时态结构的各种基本形式性质。…T.Ida研究了函数逻辑程序的一些基本性质，并在分布式系统下实现了一个函数逻辑程序设计系统。T.Ida为各种结构的执行提供了细粒度的运行机制，包括可演化程序和机制。T.Sakabe给出了一个自适应TERSS模型。在线性逻辑及其扩展方面做了许多有趣的工作，包括：1)引入时态线性逻辑(T.Ito)；2)具有局部性和时序性的线性逻辑语言(K.K.Kobayashi)；3)结合线性逻辑和并发TRSS来描述和验证实时系统(M.Okada)；4)线性逻辑程序设计语言的高效编译器(N.Tamura)。此外，K.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