>>202
>交換律を含めれば
細かいのだが、ここは、反対称律を含めなければ、だな

>つまり、(形式手法の)証明ではサブクラス(というコトバ)から人が連荘zする直感的な�意味は無視されｂ
>たとえば、仮にサブクラス(というコトバ)の代わりに机や椅子(というコトバ)で仕様が記述されていても
>(無矛盾であることを)証明できるのが形式手法であり、それが非形式手法との違いになる
この辺り、ヒルベルト流の「形式主義」の説明なら妥当だが、ソフトウェア工学の「形式手法」の
説明としては相当ズレてると思う