复杂状态程序和系统的语义模型研究

本项目的研究目标是为具有复杂状态的程序和系统建立语义模型，使之能更好支持对于这种程序或系统的定义、变换、严格的精化推导、性质证明等，支持对于这种程序或系统的分析、描述和开发。这一研究所针对的主要对象是操作复杂数据结构的程序和系统，面向对象语言和系统。研究中将特别关注由于状态的复杂性引起的各种问题，通过各种技术缓解其负面影响。要研究状态的分解和隔离屏蔽，对局部状态的推理及局部推理结果与全局状态的融合，断言与不变式在复杂状态程序与系统研究中的作用，部分状态的拥有关系与拥有关系的释放和转移，类型理论和技术在复杂状态语义模型中的作用等。还将关注软件开发领域中针对复杂状态程序和系统的实用开发技术（特别是OO技术），从语义角度研究对这些技术的支持。我们还计划研究复杂程序与系统的语义模型与实时系统和嵌入式系统的关系，与资源模型的关系和对资源推理的支持。