终止性(termination),理学-计算机科学技术-计算机软件-软件基础理论-程序理论-程序正确性,对于任意的输入,程序的执行步骤都是有限的。程序的终止性主要针对顺序程序,关心是否能够获得计算结果。具体而言,给定系统初始状态或系统输入的谓词(称为前置断言),程序具有对于给定前置断言的终止性,当且仅当若程序运行开始时系统状态或系统输入满足前置断言,则程序运行能够终止。终止性不是一阶逻辑的性质,不能归到谓词逻辑的推理,其证明手段通常基于良基集合上的秩函数的构造,将程序的终止性对应于良基集合不存在具有无穷降链的子集这一性质。