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
项目状态：
已结题

项目摘要

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针对函数式程序给出了一种将顺序程序转换为并行程序的健全并行化框架，所得并行程序比原始顺序程序运行得更快。分布式程序的验证和规范发展M. Hagiya 提出了一个有趣的想法，即验证方法的验证以及如何演化验证条件，使用时序逻辑和线性逻辑来研究弓来指定和验证实时反应系统。，他给出了时间结构的各种基本形式属性……更多 T. Ida 研究了函数逻辑程序的一些基本属性以及可执行规范的应用，并在分布式系统下实现了函数逻辑编程系统。术语重写系统（TRS）。提供细粒度的运行机制T. Sakabe 给出了自适应 TRS 的模型。 Y. Toyama 给出了 TRS 的分析和综合方法，以及证明 TRS 终止的强大过程。此外，还有一些有趣的工作。关于线性逻辑及其扩展的研究已经完成，包括 1）引入时间线性逻辑的提案（T. Ito），2）具有局部性和时间性的线性逻辑语言（K. Kobayashi），3）提案结合线性逻辑和并发TRS来规范和验证实时系统（M. Okada），4）线性逻辑编程语言的高效编译器（N. Tamura）此外，K. Kobayashi提出了一种分布式类型系统。保证无死锁的系统，S. Nishizaki 提出了一种环境演算，它是 ML 的扩展，将环境合并到 ML Less 中。