「せっかく記号を使った形式手法があるのに自然言語に戻るのか」というツイート

public.icon

それはそうと、軽量な形式手法たる型システム含む形式手法は記号の世界の中での正気はちゃんと証明してくれるが、人間様が頭を捻って作られた、自然言語で書かれた仕様とやらは一体何の正気を保証してくれるんだろう

みんなに質問形式手法って、テスト駆動開発とかが具体的なものですか?

なんで流行ってないんですか？

いくつかの水準があるっぽい

水準0

形式仕様記述を行い、プログラム自体を非形式主義的に行う。「軽い形式手法」と呼ぶ。費用対効果が早く得ることができる選択である。

水準1

形式手法を使って開発と検証を行い、より形式主義的にプログラムを生成する。例えば、仕様記述からのプログラム作成において詳細化と属性の証明を行う。高信頼システムに適した選択である。

水準2

自動定理証明によって完全に機械的な証明を行う。道具を整備するのに費用がかかるか、厳密である必要がありシステムを記述するのに手間がかかる。間違いが混入することで生じる損失に見合わなければ実施しない（例えば、マイクロプロセッサ設計の重要な部分など）

通常のシステム設計では自然言語で仕様書を書いたり、必要に応じてUML図を書いたりするでしょう。

https://gyazo.com/585ba2f66616fbe18c0514d2dee5f123

モデル検査ではこのような状態遷移システムに対して、『決済を行う前は何度でもラーメンを選び直せる』『ラーメンが未指定の注文は発生しない』といった性質が成り立つかを解析することができます。

形式手法の売り文句は設計段階や実装段階でバグを見つけることで、バグ修正のコストを下げるというものです。これは「設計」→「実装」→「テスト」の工程がはっきりと分かれているウォーターフォール開発モデルを前提にしています。

しかしながら、現代のソフトウェア開発ではアジャイル開発モデルが主流になってきています。

え、そういうこと？

形式手法を用いてもバグは０にならない

chatgpt.icon

形式手法（けいしきしゅほう）とは、ソフトウェアの設計や開発において、数学的な手法や形式言語を用いて正確な仕様や設計を表現し、それを自動的に解析したり検証したりする手法のことを指します。形式手法は、ソフトウェアの正確性、信頼性、安全性などを高めることができるため、特に高度なシステムやミッションクリティカルなシステムの開発において重要な手法となっています。

形式手法には、例えば、形式仕様言語や形式的証明、モデル検査などがあります。形式仕様言語は、自然言語やプログラミング言語では表現しにくいシステムの仕様を数学的な形式で表現するための言語であり、形式的証明は、その仕様が満たされていることを数学的に証明することです。また、モデル検査は、システムのモデルを自動的に生成し、そのモデルが満たすべき性質を検証する手法です。

形式手法は、正確性を求められる分野だけでなく、プログラマーやシステム開発者がコードを書く際にも役立ちます。形式手法を用いることで、コードの品質を向上させ、バグの混入を防止することができます。

フォーマルメソッド（＝形式手法）は、数学的に厳密に意味付けられた言語（「形式仕様記述言語」と呼ぶ）を用いて情報システム（ソフトウェア、ハードウェア等）の要求や設計等を記述し、情報システムがユーザの要求等を満たしているかなど論理的に推論するための仕組みを提供する手法である。

数学理論などによって異なる多数の手法の総称

フォーマルメソッドは、鉄道分野、航空分野、金融・セキュリティ分野など、セーフティクリティカル・システムやミッションクリティカル・システムなどにおいて、欧米を中心に実システムに対する適用事例が増えている

https://gyazo.com/24a98cc886f7d1e8bbb8a764b76a157a

https://gyazo.com/61545c84a814cddedb3598b55443f15a

え、これ絶対使ったほうがいいじゃん

https://gyazo.com/9085364fec511ac22d7f47b126036f61

なんかレベル感みたいなのがあるのか

単体・結合テスト

単体・結合テストでは、大きなシステムを小さな部分に分割して検査する。単体テストでは、 分割した小さな部分 (単体) を対象に、それに適当な入出力を与えるプログラム（モック/スタブ）を組み合わせて、 単体の反応が適切か、また単体の内部の変化が適切かといった単体の動きを外と内から見る。

https://gyazo.com/2d288f32effe58c6cb55d91f93d6a9fe

形式手法

単体・結合テストでは、システム（コード）を分割してテストしたのに対し、形式手法ではシステムを抽象化して テストするのが特徴である。

抽象度の高い階層の順に従って設計作業が 進められる（ウォーターフォール・モデル）。形式手法では、直接コードをテストするのではなく、 抽象度の高い階層のシステムの動作を検証したり、抽象度の違う階層のつながり具合を検証したりする。 これにより、早い段階 (例えば、コーディングがなされていないような場合でも) でシステムの不具合が見つかり、 また階層化されたシステム設計の整備を促進して、システム開発の効率化や、保守性を高めてくれる。

https://gyazo.com/97d8e27254acb31ea057e91b9b499009

4. 形式手法の長所と短所

長所：

形式手法は、論理に基づく厳密な検証であり、テストケースの抜けが少ない。実際、単体・結合テストで見落とされた バグが形式手法の利用により数多く発見されてきた。また、抽象化されたシステムの検証は、階層化されたソフトウェア設計との 親和性が高く、ソフトウェア設計の整備につながる。そしてその結果、ソフトウェアの保守性、拡張性が容易になる。 また、上流段階での検証を組織的に行えるので、ソフトウェアの開発が効率化される。

短所：

（現段階の）形式手法の検証ツールを使いこなすには、論理式の読み書きの能力が必要になる。 そこに敷居の高さを感じる場合が多い。

どのように形式手法を導入するか？

形式手法は、このように魅力的な長所を備えている。特に、大規模システムや 分散システムの開発でその効果は大きい。しかし一方で、克服すべき短所もかかえている。 形式手法導入のための、現段階での最良の方法は、形式手法を得意とする専門機関に導入と社内教育を 委託することであろう。その中で自社に合った形式手法の適用法をデザインし、その運用方法をアレンジし、 同時に社内教育を実施する。一連のこの大きなルーチンをこなせば、その後の形式手法の適用が円滑に進むはずである。　

想定読者として学習前の私と近い属性——すなわちコンピュータサイエンスや数学の専門教育を受けておらず、主に現場での実務と自習に頼ってきたソフトウェアエンジニアを想定しています。

形式手法というのはテストよりも抽象的に、網羅的に問題を発見できるらしい。

形式手法は数理論理学に基づいているという説明もある。わからない。普段のプログラムだってif文を書くぞ。何が違うんだ。形式化されているのが違う？　なるほど……なるほど？　そもそも形式化って何だ？　プログラムのコードは機械が読むためのものだが、それは形式化じゃないのか？　やっぱりわからない。普通のプログラミングと形式手法を隔てるものは何なんだ？

これ完全に同じでわろた

私の当初の「プログラムのコードだって形式化されているのでは？」という疑問は正解です。普段プログラマが使うプログラム言語は形式言語です。利用可能な文字集合、文法のルールが規定されており、曖昧な構文を許さない言語です。

この結果を確認したいとき、プログラマが慣れているユニットテストでは具体的なケースを列挙するしかありません。 {a:3, b:4, c:5} のとき成り立つ、 {a:5, b:12, c:13} のとき成り立つ……といったように。

なるほどね

しかし証明なら、個別のケースではなく任意の無限の直角三角形について定理が成り立つことを示せます。中学数学の証明では、直角三角形の図に補助線を引くなどの作業を通じて、すでに明らかな定義を変形させて定理を導きました。

三平方の定理を考えてみましょう。a,bの二辺と長さcの斜辺からなる直角三角形においてa2+b2=c2が成り立つという定理です。

https://gyazo.com/8eae8788e91ec550adb1d43d820afd06

中高の数学の範囲を離れると、次のように言えます。無条件に正しいと見なせる命題を公理といいます。公理に繰り返し推論規則を適用していくと定理を導出できます。その論理の筋道をつけるのが証明です。

形式手法は、ソフトウェアの正確性や信頼性を向上させるため、数学的な手法や形式的な表現を用いてシステムを設計したり検証したりする手法です。形式手法では、システムをより正確に表現するために、高次元的な数学的な概念や表現方法を用いることがあります。

一方、圏論は、数学の一分野であり、概念や構造を抽象化し、一般化することで、異なる分野や問題に対して共通の理論や手法を適用することができます。圏論では、対象や射を抽象化し、それらの間の関係を定義することで、様々な分野での共通性を捉えることができます。

時と場合に応じて（要件に応じて）論理体系を変えることはあるっぽい

たとえばアルゴリズムが仕様を満たしていることを検証したければ、その事前条件・事後条件をHoare論理を使って記述します。システムの長いライフサイクルにおける性質を検査したいときには「いずれtrueになることがある」「常にtrueのまま」といった時相論理を使った表現を使うこともできます。他

重要なのは適切な抽象度での仕様記述・モデリングです。時には表現力を制限し簡単な記述を可能にしたDSL（ドメイン特化言語）が有効な解決策になります。

ソフトウェア工学の道具としての形式手法では、形式手法とは何かという問いに、次のような説明で答えています。

数理論理学に基づく言語ならびに証明技法などからなる基礎理論を持つことに加えて、設計手法、ドメイン知識、などが関係する総合的な技術

形式手法にとって数学は基礎的な語彙である

https://gyazo.com/36158408f83e7a8b5997656ddfc3c529

https://gyazo.com/e056afb77abf5c63557f9f674d447234

結構デカめのソフトウェア開発において有効なのかな？

https://gyazo.com/3014084d013f34e1f03f3d1efcfba872

https://gyazo.com/56b7a84986185415e8a82ab0df528330

https://gyazo.com/bcff1333100a3a823f5b32bdce6bd21a

https://gyazo.com/f5b25987834fa3be3159b0256db7c2a2

https://gyazo.com/2eac28b6bb432a34c587df38fe665443

https://gyazo.com/840947782c18ccc3fc3c7113672d531f