型検査は軽量な形式手法である