org.jmlspecs.jml4.rac.runtime
Class JMLRacBigIntegerUtils

java.lang.Object
  org.jmlspecs.jml4.rac.runtime.JMLRacBigIntegerUtils

public class JMLRacBigIntegerUtils
extends java.lang.Object

Method Summary

static java.math.BigInteger	first(java.math.BigInteger i, java.math.BigInteger j) This method is used in the RAC implementation of postfix ++ and -- over \bigint's.
static java.math.BigInteger	value(java.math.BigInteger i) This method is used in the RAC implementation of prefix ++ and -- over \bigint's.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

value

public static java.math.BigInteger value(java.math.BigInteger i)

This method is used in the RAC implementation of prefix ++ and -- over \bigint's. Given \bigint bi, we translate ++bi into value(bi = bi.add(BigInteger.ONE)). The reason that ++bi is not simply transated into (bi = bi.add(BigInteger.ONE)) is that expressions cannot be used where a statement is expected where as a method call like value(...) can.

first

public static java.math.BigInteger first(java.math.BigInteger i,
                                         java.math.BigInteger j)

This method is used in the RAC implementation of postfix ++ and -- over \bigint's. E.g. given \bigint bi, we translate bi++ into first(bi, bi = bi.add(BigInteger.ONE)).