設計書の証明性について

設計書について考えてみる。あまりにも漠然としているので
そもそも「設計書」と「仕様書」の違いはなんであるのか、
設計書は「設定関係の何らかのパラメータを計算した書類」と考えれば、
非常に正確性が求められる書類と言える。
仕様書とは、頭に要件を着けて、「要件仕様書」が本来の意味であくまでも利用者や
ステークスホルダーが、要求を出す（表す）為の書類を指している。

仕様書は人間臭い情報を内蔵しているが、設計書はかなり数学的で証明（テスト）までを
含んだ側面を持つ。

では、上位工程から下流工程までの設計の関係はどうなっているのか、
人が設計書を作成し利用しているので、当然設計書にも遊びのような部分が多分にある。

そこで設計書を次のように公理的に？定義してみる。

「上位設計書」＜＝＞「下位設計書」＋「非設計要件」

非設計要件とは、デザイン等の概念で解り易く見せたり、美しく見せたりや図を使って俯瞰
したりすることを指す。
こうして考えると、上位設計書と下位設計書はある程度可換でなければいけない気がする。
下位設計は実装関係の現実世界の話しなので、HW、SWやネットワークの設計書になる。
これについても千差万別な選択肢があり、完全な可換な設計書は難しいと考えられる。
やれるとしたら、大企業がナレッジシステムを使えば可能なのか？
何故か矛盾している。

「上位設計書」＜＝＞（「下位設計書」＋「非設計要件」）＋「外部実装仕様」

これで、良いのであろうか。

話は変わりますが、UMLにも謎なところがある。
元々言語なのだから何種類もある図を完全に定義していて開発者に完璧を求めるている。
しかし、規格を考えた人は完全な証明してから、UMLを定義しているのだろうか？
労力を考慮したら、何故UMLから完全なソースコードを自動生成できないのだろうか？
（OCLの問題もあるようですが）
まだまだシステム開発が未熟で、完成形ではないからなのだろか？

結論を直接表現することは不可能でしたので、回りくどい説明になりましたが、

今の時代は、究極のスピード開発が求められているとすると、絶えず先へと前進しないといけない。
しかし、結局開発が完了したところは既にレガシーな領域になってしまいます。
これの繰り返し。
そこで活躍するコンセプトは、設計の可換性であり、これの証明であると考えています。

果たしてこんな公理的なことが可能であるのか今後も考えて行きます。