外部関数の動作、より正確にはそれらの終了を指定しようとしています。ACSLのドキュメントによると、\terminates p;
プロパティでは、述語が保持されている場合p
は関数が終了することが保証されていますが、保持されていない場合は何も指定されp
ていません。また、決して返されない関数は次のように指定できることも説明しています。
//@ ensures \false ; terminates \false ;
さらに、ACSLは\exits p;
、突然終了した場合の事後条件を指定するプロパティを提供します。だから私は疑問に思っています:
//@ ensures \false ; exits \false; terminates \false ;
関数が常に無限ループになるように指定しますか?
さらに、仕様は何ですか:
//@ ensures p ; exits q; terminates \false ;
可能な無限ループに関する手段?