13/06/02 22:55:50.61 .net
業務ロジックがどういうものか知らないけど仕様記述自体はできると思うよ
ただ形式仕様記述ができることと
論理矛盾の検出ができることの間には大きな隔たりがあるのが現状
状態の数が限られているならなんとかなるけど
状態変数に実数とか時間を持つとなると途端に検証が困難になる
13/06/02 22:55:50.61 .net
業務ロジックがどういうものか知らないけど仕様記述自体はできると思うよ
ただ形式仕様記述ができることと
論理矛盾の検出ができることの間には大きな隔たりがあるのが現状
状態の数が限られているならなんとかなるけど
状態変数に実数とか時間を持つとなると途端に検証が困難になる