抽象解釋為程序不變式的自動(dòng)化生成提供了通用的框架，但是該框架下的大多數(shù)已有數(shù)值抽象域只能表達(dá)幾何上是凸的約束集．因此，對(duì)于包含（所對(duì)應(yīng)的約束集是非凸的）析取語(yǔ)義的特殊程序結(jié)構(gòu)，采用傳統(tǒng)數(shù)值抽象域會(huì)導(dǎo)致分析結(jié)果不精確，針對(duì)顯式和隱式含有析取語(yǔ)義的循環(huán)結(jié)構(gòu)，提出了基于循環(huán)分解和歸納推理的不變式生成改進(jìn)方法。緩解了抽象解釋分析中出現(xiàn)的語(yǔ)義損失問(wèn)題．實(shí)驗(yàn)結(jié)果表明：相比已有方法，該方法能為這種包含析取語(yǔ)義的循環(huán)結(jié)構(gòu)生成更加精確的不變式，并且有益于一些安全性質(zhì)的推理．