述語抽象化によるアルゴリズムの検証 ～シェープ解析を例として