ゼロから学んだ形式手法 - DeNA Testing Blog

2020年1月に入社し、SWETの仕様分析サポートチームに加わったtakasek（@takasek）です。 仕様分析サポートチームでは、社内のプロダクト開発に対する形式手法の活用可能性を模索しています。当ブログでも、継続的に形式手法に関する情報発信をしています（形式手法 カテゴリーの記事一覧）。 この記事では、加入3か月を経てようやく形式手法の輪郭が掴めてきた私の視点から、学習前後での理解の変化について振り返ります。想定読者として学習前の私と近い属性——すなわちコンピュータサイエンスや数学の専門教育を受けておらず、主に現場での実務と自習に頼ってきたソフトウェアエンジニアを想定しています。 形式手法を学ぶ前の認識と疑問 ソフトウェアエンジニアとしての私の一番の興味関心は設計手法です。設計は、なんらかの解決したい問題に対して、ある一面を切り取った構造（モデル）を与え、そのモデルを解決の機構に落

[taka_sek]

3ヶ月の形式手法についての学びを振り返りました。初学者視点で疑問・認識の変化を追い、形式手法の掴みづらさの解消に焦点をあてました。

[tonchix]

“プログラマが日常的に頼っている型システムも「型システム入門」によれば「最も確立された軽量形式手法」” へぇー！そうなんだ

[a_suenami]

takasekさんの記事、やっと読んだ。僕も最近形式手法でいろいろやってみたいと思っているのでがんばっていきたい。

[htnmiki]

なんかおもしろいぞ

[hi-hats]

組織として形式手法を取り入れていこうとしているIT企業を他に知らない。DeNAへの好感度めちゃUP

[murashit]

いいことが書いてある

[sh19910711]

"テストの7原則によれば「テストは欠陥があることは示せるが、欠陥がないことは示せない」。その弱点をカバーできるとしたら形式手法はすごい。ただ理屈がよくわからない"

[misshiki]

“大がかりにではなくアドホックな形で形式手法を用いるアプローチは「デザイン電卓」と形容されるそうです11。形式手法に対しての大仰なイメージを払拭してくれる素敵な表現だと思います。”

[mohri]

“アドホックな形で形式手法を用いるアプローチは「デザイン電卓」と形容される”

[yarumato]

“形式手法というのはテストよりも抽象的に、網羅的に問題を発見できるらしい。テストは欠陥があることは示せるが、欠陥がないことは示せない。その弱点をカバーできるとしたら形式手法はすごい。”

[devorgachem]

形式手法はいいぞ