实代数符号计算在形式化方法中的应用

形式方法传统上基于离散数学。但实际上程序设计离不开连续变量,例如混成系统就离不开连续部件及其和离散部件之间的相互配合。近年来,形式方法中引入连续数学的研究有很多发展。例如线性程序的终止性分析,线性不变式的获取,时段演算和混成自动机的建立等。在这些研究中离不开求解非线性约束条件,或讨论系统状态的可达性及稳定性等。因此,形式方法可以使用实代数符号计算及相关工具。我国在实代数符号计算方面有不少重要贡献。