1

モジュロ演算子を合金でモデル化する方法は?

合金を使って、4 の倍数は 2 で割り切れることを証明したい....

これが私のコードです..

    //proof that 4n is divisible by 2

    module I4nDivisibleby2

    sig num {}

    fact {
        all n:num|n%4=0
    }

    assert even {
    all n : num | n%2 = 0
    }

    check even for 1

これはコンパイルされません

4

1 に答える 1

4

ライブラリ定義rem関数を使用する必要があります。この関数は 2 つの int を受け取るため、 ;remのインスタンスに対して呼び出すことはできません。num代わりに、次のようなことができます

module I4nDivisibleby2

sig num { 
  val: Int
}

fact {
    all n:num | rem[n.val, 4] = 0
}

assert even {
    all n : num | rem[n.val, 2] = 0
}

check even // => no counterexample found
于 2013-09-25T19:38:46.413 に答える