A Study on Program Verification Systems based on Analytic Semantics

实时程序系统的验证研究是当代程序理论的重要领域之一。在本研究项目中，研究人员基于分析语义学和分析等价理论，发展了几种逻辑程序和过程性程序的验证形式，称为SOFA、包络理论和时态算法。这些是为了分析和验证控制离散的某些连续的物理或其他外部系统的程序。每一种形式主义都描述了对观察时间中下一个动作的唤醒时间的分析。研究人员还将音乐信息处理作为实时、高智能程序系统的实例之一进行了研究。他们已经开发并试验了实时控制性能系统。这些系统的设计基本上是困难的，因为这些系统的实时性，以及人类独奏者的身体动作和反应的性质到目前为止还没有被很好地理解。此外，声学三角钢琴在每次输入MIDI事件后都有0.5[秒]的物理声音延迟(即相应按键的动作)，因此程序必须预测人类在涉及钢琴的伴奏系统中的表现，这也是使设计更加复杂和困难的另一个因素。为了应对这些情况，解决现代软件技术带来的各种问题，他们对这些系统的规范进行了逻辑表示，并使用这些形式化来验证这些正确性。

A study of verification of realtime program systems are one of the most important fields for contemporary program theory. In this research project, the investigators have developed several verification formalisms for logical and procedual programs, named SOFA, the envelope theory and the tense arithmetic, based on the analytical semantics and the analytical equivalence theory. These are to analyze and verify programs that controls discretely certain continuously physical or other external system. Each formalism describes analysis of the wake-up time of the next action from an observation time. We obtain the actual rational time value when the next action will rise, so that verification can be easier and more precise.The investigators have also researched music information processing as one of the examples of the realtime and highly intelligent program systems. They have developed and experimented realtime controlled performance systems. The design of these systems is essentially difficult because of the realtimeness and the fact that the nature of physical action and reaction by human soloists has not been understood well so far. Besides, especially, the acoustic grand piano has 0.5[sec.]delay of physical sound(i.e., the action of the corresponding key)after each input of MIDI event, so that the program must forecast human's performance in the accompaniment systems involving piano, which is another factor to make the design more complex and difficult. In order to cope with these situations and to solve various problems incurred upon with modern software techniques, they have represented specifications of these systems logically and verify these correctness using these formualisms.