プログラムが、定められた性質$F$を満たすかどうか、は一般に判定不能