0

この表記の構文を完全に理解するために行くことができるチュートリアルを知っている人はいますか？

/* value definition */
abstract typedef <int, int> RATIONAL;
condition RATIONAL[1] != 0;

/* Operator definitions */

abstract equal( a, b )                        /* written a == b */
RATIONAL a, b;
postcondition equal == ( a[0] * b[1] == b[0] * a[1] )

abstract RATIONAL makerational( a, b )      /*  written [a, b] */
int a, b;
precondition b != 0;
postcondition makerational[0] * b == a * makerational[1]

abstract RATIONAL add( a, b )            /* written a + b */
RATIONAL a, b;
postcondition add == [ a[0] * b[1] + b[0] * a[1], a[1] * b[1] ]

abstract RATIONAL mult( a, b )
RATIONAL a, b;
postcondition mult == [ a[0] * b[0], a[1] * b[1] ]
4

2 に答える 2

0

有理数、つまりある整数を別の整数で割ったものを知っていれば、その表記法を理解するのは難しくありません。

見たことはありませんが、有理数 (分数) の性質から、角括弧のインデックス付けが 2 つの整数のベクトルとしての表現であることは明らかです。

次に、通常の数学表記では、

upper( rational( a, b ) ) = a
lower( rational( a, b ) ) = b

equal( r1, r2 ) = (upper(r1)*lower(r2) eq upper(r2)*lower(r1) )
add( r1, r2 ) = rational(upper(r1)*lower(r2)+upper(r2)*lower(r1), lower(r1)*lower(r2))
mul( r1, r2 ) = rational(upper(r1)*upper(r2), lower(r1)*lower(r2))

乾杯、

于 2011-02-08T01:42:53.830 に答える
-1

makerational は本当に再帰的に見えますよね! 「C および C++ を使用したデータ構造、Yedidyah Langsam、Moshe J. Augenstein、および Aaron M. Tenenbaum 著、第 2 版」という本には、良い議論があります。それは最初に示します

事後条件 makerational[0] == a; makerational[1] == b;

次に、1/2 と 2/4 が等しいと見なされるべきであるという事実について議論し、定義を修正します。私はそれを次のように読むことができると思います: 結果の RATIONAL に b を掛けた [0] 要素は、結果の RATIONAL に a を掛けた [1] 要素に等しくなければなりません。

于 2015-10-31T17:03:00.197 に答える