通过safety check寻找不满足当前ranking的终止执行。如果safety check通过,有两种可能:
- 程序确实是终止的,且当前的ranking是valid的
- 程序终止的那部份可以用当前的ranking刻画,但是还存在不终止的trace。
因此,在算法2中,还需要最后检查ranking对整个loop是否是valid的,这也是通过safety check完成。
两次safety check有细微但是很重要的区别:当用于找出终止的反例时,断言在循环之外,表明反例必然是终止的;当用于验证ranking时,断言在循环体内,此时反例要么代表非终止的trace的前缀,要么代表不满足当前ranking的终止trace(但这已经被算法2排除)。