誰でもできるソフトウエア開発の要件定義＆ドメイン分析およびクラス図の科学的アプローチ

確定申告の作業が終了し、契約している税理士さんに後は全てお任せした。

　
　
有価証券の確認作業も終了。
　　
資料や書籍も整理した。

書籍を整理していたら論理学のタブローの書籍があったので、本を整理しながらまだ憶えているか、直ぐに解けるか、整理しながらちょっとやってみた。

　
　
述語論理やタブローによる形式化や証明は大学の教養課程で学ぶ「論理学」の授業で使う教科書で間にある。
　　

なので、理学部や工学部系の学生や卒業生なら基本的には誰でもできる。
大抵、学部１学年の時に習うはず。

述語論理の形式化に関連する知識は、ソフトウエア開発の要件定義やドメイン分析およびクラス図の作成に、直接に関わってくる重要事項だ。
　
まず命題を述語論理形式で表現する演習問題があったので、さっそく試した。

　　
『勉強しない学生は落第する』
　　

論理学の形式化でもそうであるが、要件定義やドメイン分析では前提として「議論領域」を明確にする必要がある。

　そうしないと、クラス図が変わってくる。
　
議論領域：対象の集合を人間全体の集合とすると：
Student(x):x は学生
Study(x):xは勉強する
Fail(x):xは落第する
　　

(∀x)[( Student(x) ∧ ¬Study(x))⇒Fail(x)]
　　

これは楽勝だな。
　　

もう１丁。

　　
『仮に論理学を履修するが物理学を履修しない学生がいて、そして、論理学を履修する学生は誰でも数学も履修するなら、論理学を履修するが、数学を履修しない学生がいる』
　　

これはちょっと長くて複雑だ。

　　
議論領域を人間全体の集合ではなく、「ある大学の学生全体の集合」とすると、確実に論理式が変化する。 「Student(x) ∧」を考慮する必要がない。

　
　
対象の集合を人間全体の集合とすると、ある大学の学生でないならば定義域外となるので、関　連(関数：写像は)が部分関数になる。
　

しかし、定義域を絞ったので全関数となる。
　

議論領域：ある大学の学生全体の集合とすると：
Logic(x):xは論理学を履修する
Physic(x):xは物理学を履修する
Math(x):xは数学を履修する
　
結局、

　
　
[(∃x)( Logic(x) ∧ ¬Physic (x)) ∧ (∀x)( Math(x) ⇒Physic(x))] ⇒ (∃x) Logic(x) ∧ ¬Math(x)
　

になる。

『科学的モデリング』による高階述語を利用した複雑なクラス図の考え方

UMLで関連を検討する科学的なアプローチをちょっと紹介。

ケースとして：
　
　各官庁が補助金を出す大学を選ぶ時、まず候補大学を選んで、その中なら最終的に補助金を出す大学を選出する
　　

場合を考える。
　
関連は命題表現(関係述語)であり、これは同時に「演繹」であり「写像」であるから、最初の関連は論理表現では：
　　
『 候補に選出する(官庁 , 大学) 』
　
と記述できる。
　
最終的に求めたい関連(写像)は
　　
『 選定する(官庁、大学) 』
　
であるが、定義域に気を付ける必要がある。
　　

まずこの関連(写像)の定義域は、官庁、大学は最初の述語と同じ変数を指すので、『 候補に選出する(官庁 , 大学) 』を満たす大学から選ばなければならない。

　
　
結局：
　　
『 選定する(候補に選出する(官庁 , 大学))』
　　

と引数が、最初の関連(写像)になる高階述語となる。ここがポイント。

　　
UMLによるクラス図では、これは関連クラスと関連クラスを繋ぐことで表現できる。
　　

この方法は「論理による問題解法」と言う方法でキチンとした学問体系がある。＊でも奥は深く専門性は高い。
　
Prolog(やLisp)でプログラムを組むエンジニアは良く知っていると思う。

どんな複雑で面倒な制約を持つクラス図もサクサクと描けます。

リアルタイム制御系の分析・設計ツール

リアルタイム制御系の分析・設計ツールを色々操作している。
　
クルーズコントロールシステムのシミュレーション。

『科学的モデリング』による自動シミュレーションと妥当性確認

『科学的モデリング』でモデルの自動シミュレーションと妥当性確認を行った。

数学・論理学およびソフトウエアの定理や原則を用いるので、UMLによるモデル作成も時間がかからない。

自動シミュレーションによる妥当性確認自動の作業は、もっと短く5分と掛からない。
　
今日の作業は自動によるシミュレーションと妥当性確認そのものではなく、『科学的ソフトウエア開発アプローチ』のプロセスの完全自動化の確立の準備作業が目的。
　

構成管理やテストも自動化すつように確立していく。

　
大切なのは単なるツールによる変換ではなく、数学的・論理学的な正当性や充足性や妥当性を持つモデルを作成することで、自動シミュレーションと自動妥当性確認および自動検証が行えるようになることである。

　
真となる条件を設定するので、演繹的なので作業やプロセスが健全(Soundness)かつ妥当(Valid) である判断できる。

一度実施した自動シミュレーションと妥当性確認は自動でシナリオが記録されるので、シミュレーションやテストケースとして何度でも自動でAutomaticに行える。

このテストシナリオには、わざとエラーとなる様になっているが、自動によるシミュレーションと妥当性確認で、正確に検出することができた。

　
この時は30秒と掛からない。
　

Alloyを用いれば、自動で検証(Verification)や反例チェックも行える。

モデルが複雑で高度になればなるほど、効果を発揮する。リアルタイムシステムや制御システムや組み込みシステムには不可欠。

『科学的モデリング』による「関連」のモデリングと表現方法

現代の数学やソフトウエア開発は「モノ」に注力するのではなく、「コト(関数／演繹／命題関数)」に注力する記述が最重要となる。

　
　
UMLによるモデルは「自然言語の文章」「述語論理による論理式」「集合と写像」「行列」でも同じ事が表現できる（ただし、本質的にはどの表現も同じ内容を表現するが、表現方法の違いで分かり易さなどが異なる場合はある。）

「述語論理による論理式」「集合と写像」でも同じ事が表現できるのは、UMLやオブジェクト指向が数学・論理学を土台にしてるから当然である。

　
　
だから、UMLやオブジェクト指向が数学・論理学であること無視してはダメである。
　　

それでは工学にならない。

　

また数学的なことを守らないと自動化による作業が困難である。

『The Goal』で有名なゴールドラットの実践用書籍

古い本だがユニークな内容で今も持っている。

『The Goal』で有名なエリヤフ・ゴールドラット氏の「制約条件の理論（TOC）」の実践版の書籍である。

TOC理論と共に「思考プロセス」もゴールドラット氏は提唱しているが、それも掲載されている。

　
　
CD-ROMに専用のアプリが付いているが、今のOSでは動かない。

Isabelle2014～定理証明系言語処理系

StandartMLの流れをくむ Isabelleの処理系。

　
MLなんて今でも使うのかと思うけど、結構使うと思う。
Ocamlもほとんど同じだし。

　

　
ところで、Isabelleという名称から学生の頃に日本でも人気があった「イザベル・アジャーニ（Isabelle Adjani） 」をいつも連想する。
　
確か高校生になりたての頃、デザイナー高田賢三が監督した「エーゲ海に捧ぐ」に主演してた。
この映画の主題歌はあのジュディ・オングの「魅せられて」だ。

『科学的MDA』による自分自身を 自動検証可能なモデルおよびコード

UMLで作成されたモデルやプログラム言語で書かれたコードは、自分自身を自動で検証可能なモデルおよびコードを作成することができる。
　
勿論、何から何までFull自動で検証は無理だし、ビジネスルールや定義を明確にUMLモデルに記述し、「正当性」「妥当性」「充足性」等をセットすることでツールを利用することで可能なってくる。
　
先日、簡単な例題でデモをした。
　
現在のソフトウエア開発は、そもそも要件定義や分析で「正当性」「妥当性」「充足性」の検討をしていないので、本当の要件分析やシステム分析が行われていない。
　
そのため、やたらUMLで図や資料を作成し、不適切なレビューやテストで開発を進めているところにむしろ問題がある。
　
本質的な検討事項無視して、モデル作成やレビューやテストをしても効果は出ない。
　
そのためには、形式的なアプローチを上手く実開発に取り組むための工夫が必要である。

『科学的モデリング』による『科学的MDA』アプローチ～モデルの「充足性(Satisfiability)」「適用可能性(Applicability)」「正当性(Correctness)」「妥当性(Feasibility/Validity)」

『科学的モデリング』による『科学的MDA』アプローチ ～モデルの「充足性(Satisfiability)」「適用可能性(Applicability)」「正当性(Correctness)」「妥当性(Feasibility/Validity)」

人工知能やSATソルバエンジンなどの進歩で、モデルの「充足性(Satisfiability)」「適用可能性(Applicability)」「正当性(Correctness)」などを持つ自動検証とコード生成が可能になってきた。
 
『科学的モデリング』では、その必然的帰結として『科学的MDA』アプローチになる。
 
お絵かきモデルから脱却するには、モデルの作成はもちろんMDA(モデルドリブン開発)でも「充足性(Satisfiability)」「適用可能性(Applicability)」「正当性(Correctness)」「妥当性(Feasibility/Validity)」について真正面から向き合わないといけない。
 
実際に、国際規約で「充足性(Satisfiability)」「充足性(Satisfiability)」「適用可能性(Applicability)」「正当性(Correctness)」「妥当性(Feasibility/Validity)」」で重要視されている。
 
そうしないとエンジニアリングではない。分析や設計すべき重要事項が完全に欠落していまう。
 
『科学的MDA』アプローチは、「充足性(Satisfiability)」「適用可能性(Applicability)」「正当性(Correctness)」「妥当性(Feasibility/Validity)」が全く考慮されていない単なる「お絵かきモデル」から自動コード生成をするMDAとは異なり、リファイメント(Refinement)の考えを自動あるいは半自動で実現するアプローチとなる。
 
リファイメントは、下向き模倣(Down Simulation)と前向き模倣(Forward Down Simulation)あるいはその併用やいくつかの課題があるが、「抽象化関数(Abstruction Function )が求めることで、上位フェーズのモデルと下位フェーズのモデルの対応関係が数学的に行える。
 
まぁ、理想的にはいかない部分もあるが、このようなリファイメント(Refinement)の考え方や自動検証の知識は不可欠と思う。
分析、設計および実装の開発速度と品質が大きく異なるからである。

『科学的モデリング』による≪Refinement≫と≪Validation≫

上位モデルから下位モデルへの正しい作業を少しでも数学的(形式的)に実施するための具体的な方法の整理をしている。
　
雑駁に言ってしまえば≪Refinement≫と≪Validation≫。
　
かなり厳密な方法は開発現場に導入するには無理があるから、半形式的にならざる負えないが、それでも格段に生産性と品質が向上する。
　
一方で、現在のMDAは、形式的なRefinementの考え方がごっそり欠落しているものが多く、これでは単にツールによる自動化の手間しかメリットが得られない。既にある殆んどのMDA方法論はこのタイプだ。
　
これでは意味が無い。
　
Refinementにも垂直(Vertical)と水平(Horizontal)があるが、理想はなるべく垂直Refinementにしたいところだが、現実の現場の都合やプログラム言語の機能を考えると水平Refinementの性質が強くなるだろう。
　
ごく簡単な仕様とUMLクラスと妥当性のシナリオを用いて、幾つかの仕様記述言語による比較と考察を行う。
　
関連のナビゲーションは相手先のインスタンスあるいはインスタンスの集合が存在しない場合は、OCLやVDM++は、undefinedが∅が返されるが、Alloyにはこの区別がない。つまり部分関数の述語(早い話が関連や演算)の考え方にも違いがある。
　
クリーネ論理系(Kleene Logic)の3値論理の取り扱いも、OCLやVDM++は『強い論理』を採用している。

仕様仕様の妥当性と分類子の正当性を保証するモデル

今日はトレーニングとコンサルテーションで説明する『科学的モデリング』の数学的な関連の分析と設計および実装の資料を作成した。

関連は数学の写像であるが、関連の両端のクラス(集合)の定義域と値域が重要になる。

各操作はやはり写像であるから「特性方程式(characteristic equation)」を指定し定義域を明記する必要がある。

以上から、仕様仕様の『妥当性』を満たし、分類子の『正当性』を保証するには、『意味論』を盛り込んだモデルにする必要があるが、それには述語論理演繹の式を使うことになる。

シミュレーションとコード生成も完了。:-)
これによりテストケースも自動的に生が可能となる。

そのようなモデルの描き方と論理式の書き方の初歩の解説をした。

第8回『科学的モデリング』技術コラム公開～クラスと型の違い＆型の「論理状態空間」

------------------------------------------------------
第8回『科学的モデリング』技術コラム公開
-------------------------------------------------------
第8回『科学的モデリング』技術コラムを公開いたします。
http://hsc-i.com/TechnologyColumn.html
 
■一流モデラーになるための必修知識
　・継承関係の数学的設計アプローチ
　・タイプ(型)の「論理状態空間」と継承
　・タイプ(型)の「論理状態空間」の「同型」「拡張」「特殊化」
　・『科学的インスペクション』＆『科学的テスト』

分かり易い図と具体的なクラス図およびコードイメージをふんだんに使って”やさ～しく”解説しました。
サクサク読み進めることができるように解説しました。

＊第0回～第7回までの技術コラムも公開中です。

科学的モデリングアプローチ：『Visitorパターン』のモデル

教育用に科学的モデリングアプローチによる『Visitorパターン』のモデルの資料作成。

　
『Visitorパターン』は、「関心事の分離(separate of concern)」として、データーと処理をあえて分割して別々のクラスとして持つパターン。
　
この『Visitorパターン』は、かならず理解しておきたいパターンである。
　
『Visitorパターン』は実は奥が深く「型理論」の話題とも結びつく。
「共変化」継承である。
　
それから、このパターンのポイントは、いわゆる『ダブルデイスパッチ』よばれる方式である。
　
デザインパターンはほとんどが継承を利用するので、正確な継承の理解がまずは大切となる。

s