module pind.samples.ja.invariant.invariant_2;

interface Iface {
    int[] func(int[] a, int[] b)
    in {
        writeln("Iface.func.in");

        /* このインターフェースメンバー関数は、
         * 2つのパラメータの長さが等しいことを要求する。 */
        assert(a.length == b.length);

    } out (result) {
        writeln("Iface.func.out");

        /* このインターフェースメンバー関数は、
         * 結果の要素数が偶数になることを保証する。
         * (空のスライスも、
         * 要素数が偶数であるとみなされることに注意する。) */
        assert((result.length % 2) == 0);
    }
}

class Class : Iface {
    int[] func(int[] a, int[] b)
    in {
        writeln("Class.func.in");

        /* このクラスメンバー関数は、
         * 少なくとも1つのパラメーターが空である限り、
         * 長さが異なるパラメータを許可することで、祖先の前提条件を緩和する。 */
        assert((a.length == b.length) ||
               (a.length == 0) ||
               (b.length == 0));

    } out (result) {
        writeln("Class.func.out");

        /* このクラスメンバー関数は、追加の
         * 保証を提供する: 結果は空ではなく、
         * 最初の要素と最後の要素が等しいことを保証する。 */
        assert((result.length != 0) &&
               (result[0] == result[$ - 1]));

    } do {
        writeln("Class.func.do");

        /* これは、'in'と'out'ブロックが
         * どのように実行されるかを示すための
         * 人工的な実装である。 */

        int[] result;

        if (a.length == 0) {
            a = b;
        }

        if (b.length == 0) {
            b = a;
        }

        foreach (i; 0 .. a.length) {
            result ~= a[i];
            result ~= b[i];
        }

        result[0] = result[$ - 1] = 42;

        return result;
    }
}

import std.stdio;

void main() {
    auto c = new Class();

    /* 以下の呼び出しはIfaceの事前条件を満たさないが、
     * Classの事前条件を満たしているため受け入れられる。 */
    writeln(c.func([1, 2, 3], []));
}