久しぶりに勉強してます。

 

最近忙しくて仕事さぼれないw

 

今まで仕事の合間に勉強してたんですがw

 

いやーーーもう少し早く起きて作業するか・・・w

 

 

今回は仕事の効率を上げたくて勉強しました。

 

この分の給料くれw

 

あのー仕事してて効率が悪いとか自分の中でダメだと思う部分ってあるじゃないですか?

 

私は最近、設計業務とかでセンスがないなと感じることが多々あるので設計業務で知っておくべきことを勉強しました。

 

まず、私のざっくりとした業務内容なんですが。

 

こういうシステムを作ってください~

 

って言われて

・仕様検討

・調査

・開発

・テスト

みたいな感じでリリースするんですが

 

 

・仕様検討部分が不安定なんですよね

 

なんとなくこれでいいだろう!

 

って考えていざ作ってみたら

 

あれ、これはおかしい?

 

ってなって作り直したりすることがあります。

 

リリースまでは早くできても、結局考慮されていない部分で修正をする羽目になったりします。

 

そうするとリリースまでの工数が少なくても修正分の工数が追加されるため、意味がなくなってしまいます。

 

今の職場ではそこまで大きなシステムを任されているわけではないので、仕様検討+開発を同時進行に進めていますが

現状の方法は明らかに悪い設計方法です。

 

そんなとき、形式手法を使います。

 

 

結構システム作っているのに今更形式手法の勉強とかめちゃくちゃ怒られそうです・・・・w

 

形式手法はコーディングしたものをテストするのではなく、コーディングするまえの抽象的な状態をテストする方法です。

 

これによりコードを書かなくても不具合や曖昧な点に気づくことができます。

 

形式手法はモデルチェックと自動定理証明の2つの手法に分けることができます。

 

モデルチェックは主に抽象的なシステムの 動作の検証を行います。

 

自動定理証明は抽象度の違う階層のつながりを検証を行うみたいです。

 

それぞれツールがあってそちらを使って作成できるみたいなので、試してみようと思います。

 

モデルチェックのツールSPINの例

active proctype Server() {
  do
  :: (API 1の事前条件) -> API 1の処理
  :: (API 2の事前条件) -> API 2の処理
  od;
}

こんな感じらしいです。

 

なんか見てみた感じ結局コーディングと変わらないんじゃないか?って思ってしまうんで使って理解しようと思います。

 

 

んじゃ