VDM++

だいぶ文法がわかってきたので、簡単なクラスを作ってみました。
まったくの未開の大陸なので、すべてが手作りから始まります。
例えれば、すらないC言語です。まぁ、面白い半分、苦労も多々。

/**
 * 有理数のクラス
 *   分子、分母は整数である。
 *   分母は０になることはありえない。
 *   分子と分母が割り切れる場合は簡単にする。
 *   分母が負の場合、両方にマイナスを掛け、分母は常に正になるようにする。
 *
 * 固定小数点演算もこのクラスを使えば正しく計算できる。
 * 例えば、1.05（消費税）は new Rational(105,100)として計算すればよい。 
 *
 * VDM++では、有理数は内部的には実数と同じ扱いになっているため、望む機能が得られない場合がある。
 * このクラスを使えば、正しい有理数が使えるようになる。（できれば言語側で対応して欲しいのだけれど）
 * 参考:SICP2nd
 * @author A-san
 */
class Rational
instance variables
    public 分子:int := 0;
    public 分母:int := 1;
    inv 分母 > 0;

operations

public Rational: int * int ==> Rational
Rational(a,b) ==
    let 
        gcd = GCD(abs a, abs b)
    in (
        if b > 0 then (
            分子 := a div gcd;
            分母 := b div gcd
        ) else (
            分子 := -a div gcd;
            分母 := -b div gcd
        );
        return self
    )
pre b <> 0;

public get分子: () ==> int
get分子() == return 分子;

public get分母: () ==> int
get分母() == return 分母;

public toReal: () ==> real
toReal() == return get分子() / get分母();

/**
 * 有理数を "分子/分母"の形で表示する.
 * 分母が1の場合は"分子"の形で表示する。
 */
public toString: () ==> seq of char
toString() == 
    is not yet specified;   

functions
public static add: Rational * Rational -> Rational
add(r1, r2) ==
    new Rational(
        r1.get分子() * r2.get分母() + r2.get分子() * r1.get分母(),
        r1.get分母() * r2.get分母()
    );

public static sub: Rational * Rational -> Rational
sub(r1, r2) ==
    new Rational(
        r1.get分子() * r2.get分母() - r2.get分子() * r1.get分母(),
        r1.get分母() * r2.get分母()
    );

public static mul: Rational * Rational -> Rational
mul(r1, r2) ==
    new Rational(
        r1.get分子() * r2.get分子(),
        r1.get分母() * r2.get分母()
    );

public static divide: Rational * Rational -> Rational
divide(r1, r2) ==
    new Rational(
        r1.get分子() * r2.get分母(),
        r1.get分母() * r2.get分子()
    );

public static equals: Rational * Rational -> bool
equals(r1, r2) ==
    r1.get分子() = r2.get分子() and r1.get分母() = r2.get分母();

/**
 * 文字列から有理数を生成する.
 * "分子/分母"の形であること。'/'以降がない場合は、分母が１とする。
 */
public static parse: seq of char -> Rational
parse(s) == is not yet specified;


/**
 * 最大公約数(Greatest Common Divisor)
 * ユークリッドの互除法.
 */
functions
public static GCD: nat1 * nat1 -> nat1
GCD(a,b) ==
    if b = 0 then
        a
    else
        GCD(b, a rem b);

end Rational