A Research on Program Understanding Based on Simulation on a World Model and its Application to Prorram Development

提出了一种基于领域世界模型模拟的程序理解框架，并通过该项目开发了使用程序理解机制的程序验证系统，传统的程序理解系统具有关于程序的各种模式的知识，他们试图通过将适当的模式与程序的每个部分进行匹配来理解程序。然而，为了理解程序，不仅需要考虑程序的源代码，还需要考虑程序操纵的领域世界。因此，我设计了一个程序理解系统，它有一个领域世界模型，可以在这个模型上模拟程序。通过观察模拟的领域世界模型，系统能够把握程序的角色，选取程序控制汇编语言编写的机器作为目标，构建了一个实验系统，并提出了一个基于地形图理解框架的程序验证系统。该系统具有根据提到机器的状态或运动的词汇表检查程序是否满足其规范的能力。该系统处理一个包含约5000个步骤的微波炉等电器指令的示例程序，并验证它是否满足诸如“烹饪时，如果门打开，则振荡器应该关闭”的规范。

A farmework of program understanding based on simulation on a domain world model is proposed and program verification system using the program understanding mechanism is developed through this project.Conventional program understanding systems have knowledge about various patterns of programs and they try to understand programs by matching appropriate patterns with each part of programs. However, in order to understand programs, it is necessary to consider not only the source codes of the program but also the domain world manipulated by the program. Therefore, I design a program understanding system which has a domain world model and can simulate programs on the model. By observing the simulated domain world model, the system can grasp roles of programs.I picked up programs to control machines written in assembly languages as a target, and construct an experimental system.Moreover, I propose a system to verify programs by using the framework of the orogram understanding. The system has an ability to check whether a program satisfies its specification in terms of vocabularies mentioning states or motions of a machine. The system processes an example program containing about 5000 steps of instructions for electric appliances such as microwave oven, and verifies that it satisfies the specification such as "while cooking if the door opens then the oscillator should turn off".