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

提出了一种基于领域世界模型仿真的程序理解框架，并利用该程序理解机制开发了程序验证系统。传统的程序理解系统了解程序的各种模式，并试图通过将适当的模式与程序的每个部分相匹配来理解程序。然而，为了理解程序，不仅需要考虑程序的源代码，还需要考虑程序所操纵的域世界。因此，我设计了一个具有领域世界模型的程序理解系统，并可以在该模型上对程序进行仿真。通过对模拟域模型的观察，系统可以掌握程序的角色。我选择了用汇编语言编写的控制机器的程序作为目标，并构建了一个实验系统。此外，我提出了一个系统，以验证程序采用orogram understanding框架。该系统有能力检查一个程序是否满足它在提到机器状态或运动的词汇表方面的规范。该系统处理一个包含微波炉等电器约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".