ADT仕様

Question

私はこの表記の構文を完全に理解するためのチュートリアルを知っていますか？

/* 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] ] 

Answer 1

あなたは有理数は、他で割った、すなわち1つの整数であるものを知っているなら、それはその表記法を把握することは困難ではありません。

これまでは見たことがありませんでしたが、有理数（分数）のプロパティから、角括弧のインデックス付けは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)) 

乾杯& HTH、

Answer 2

makerationalは、本当に再帰しませんね！ 「C and C++を使用したデータ構造、Yedidyah Langsam、Moshe J. Augenstein、Aaron M. Tenenbaum、第2版」は良い議論をしています。最初に表示されます

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

次に、1/2と2/4は等しいとみなされ、定義が改訂されるべきであるという事実について論じる。私はそれが次のように読むことができると思う： 結果のRATIONAL時間bの[0]要素は、結果RATIONALの[1]要素と等しくなければならない。