プログラムの構造を表す方法はたくさんあります (UML クラス図など)。プログラムを厳密に数学的方法で記述する慣習があるかどうかに興味があります。私は、この目的のために数学的表記法を使用することに特に興味があります。
例: クラスは、セット (フィールド、プロパティ) および関数 (セットの要素を操作する) として表されます。親クラスのフィールドは、子クラスのサブセットです。関数は、このように見える必要がある疑似コードで記述されています...
2282 次
10 に答える
2
于 2009-10-27T18:41:01.913 に答える
1
関数型プログラミングを探しています。いくつかの関数型プログラミング言語があり、それらはすべてラムダ計算と呼ばれる基本的な数学的理論に基づいています。LISP などの関数型プログラミング言語で記述されたプログラムは、それ自体を数学的に表現したものです。;-)
于 2010-01-08T16:15:19.677 に答える
1
すでに言及されているZは、ほとんどあなたが説明しているものです。オブジェクト指向モデリングにはいくつかのバリエーションがありますが、クラスをモデル化する場合は、「標準の Z」スキーマでかなり遠くまで到達できると思います。
Z に触発された新しいAlloyもあります。その表記法は、おそらくオブジェクト指向に少し近いです。また、分析可能です。つまり、作成したモデルが特定の条件を満たすかどうかを確認できますが、プロパティが保持されていることを証明することはできず、有限の範囲内で反論を試みるだけです。
記事Dependable Software by Designは、利用可能な同様のツールの表とともに、Alloy とその同類の優れた紹介です。
于 2009-10-27T19:43:50.257 に答える
1
はい、フロイド・ホーア論理があります。
于 2009-10-27T18:36:39.393 に答える
1
方法はたくさんありますが、デフォルトの数学的概念では構造を表現できないことが多いため、構造を表現するのに不便な方法がほとんどだと思います。主な例外は、もちろん関数型プログラミング言語です。フォールド (カタモルフィズム)、群、代数などについて考えてみましょう。
命令型プログラミングについては、(純粋で拡張された) ラムダ計算集合論と (一次) 述語論理を使用する Z の存在を知っています。しかし、私はそれが非常に便利だとは思わない。構造を表現するために数学を使用することの唯一の利点は、それについて証明できるという事実です。しかし、それを行いたい場合は、JML、Spec#、または Eiffel を見てください。
于 2009-10-27T18:37:26.133 に答える
1
何を達成しようとしているのかにもよりますが、特定の言語でこの道を進むと、問題が発生する可能性があります。
たとえば、C++ FAQ Liteの円と楕円の議論を参照してください。
于 2009-10-27T18:38:55.567 に答える
1
この本は、演繹法をプログラミングに適用し、プログラムを動作させる抽象的な数学的理論に関連付けます。[...]
Alexander Stepanov と Paul McJonesによるElements of Programmingは、あなたが探しているものにかなり近いと思います。
概念とは、型で定義された手続き、型属性、および型関数の存在とプロパティに関して記述された、1 つまたは複数の型の要件の記述です。
于 2009-10-27T18:47:33.083 に答える
0
実際にプログラムまたはその操作を記述する数学言語があります。初期状態を取得し、目的のターゲット状態に到達するまでこの状態を変換します。変換により、実行する必要があるプログラム コードが生成されます。
Hoare ロジックに関するウィキペディアの記事を参照してください。
基本的な考え方は、すべての関数 (それをクラスに入れるか古いスタイルの関数に入れるかに関係なく) には、事前条件と事後条件があるということです。>= 0たとえば、前提条件は、要素を持つ配列があることです。事後条件は、すべての要素 [i] がすべての i <= j に対して <= element[j] でなければならないことです。
通常の説明は、「関数が配列をソートする」です。ただし、数学用語を使用すると、入力 (事前条件に一致する必要があります) を出力 (事後条件に一致する必要があります) に変換できます。
特により複雑なプログラムの場合、使用するのは少し扱いにくいですが、いくつかの例は非常に印象的です。多くの場合、結果として非常にコンパクトなコードが得られます。これは非常に複雑に見えますが、最初の試行では機能します。
于 2009-10-27T18:47:45.050 に答える
0
プログラミングの代数を提案したいと思います。これは、リレーショナル代数とガロア接続を使用した、プログラムへの計算アプローチです。
このトピックにさらに興味がある場合は、Shin-Cheng Mu と José Nuno Oliveira による素晴らしい論文 (スライド) をご覧ください。
リレーショナル代数と一次論理を使用すると、 Alloy、関数型プログラミング、および Design by Contract (オブジェクト指向プログラミングに簡単に適用できます) との相乗効果もあります。
于 2013-02-24T02:07:08.423 に答える