org.jmlspecs.jml4.rac.runtime
Class JMLRacUtil

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

public class JMLRacUtil
extends java.lang.Object

Method Summary

static boolean	checkErr(java.lang.Class c, JMLAssertionError e) Under the old semantics, ensure that e is an instance of c.
static boolean	matchCause(java.lang.Class c, JMLAssertionError e)
static boolean	newSem()
static boolean	nonNullElements(java.lang.Object[] a)
static boolean	oldSem()

Methods inherited from class java.lang.Object

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

Method Detail

nonNullElements

public static boolean nonNullElements(java.lang.Object[] a)

newSem

public static boolean newSem()

oldSem

public static boolean oldSem()

matchCause

public static boolean matchCause(java.lang.Class c,
                                 JMLAssertionError e)

checkErr

public static boolean checkErr(java.lang.Class c,
                               JMLAssertionError e)

Under the old semantics, ensure that e is an instance of c. Under the new semantics, ensure that e is an instance of JMLEvaluationError and [soon to be added] that e.cause() is an instance of c.