de.uka.ilkd.key.util

Class Assert

java.lang.Object

de.uka.ilkd.key.util.Assert

public final class Assert
extends java.lang.Object

Special assert statements intended for use with KeY. Raises AssertionFailure (which is a subtype of Exception) instead of AssertionError.

Author:

daniel

Constructor Summary

Constructors

Constructor and Description
Assert()

Method Summary

Modifier and Type	Method and Description
static void	assertEqualSort(Sorted t1, Sorted t2) Check whether two terms (or other sorted objects) are of the same sort.
private static boolean	assertionsEnabled()
static void	assertSubSort(Sorted t1, Sorted t2) Check whether the sort of t1 is a subsort of the sort of t2.

Methods inherited from class java.lang.Object

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

Constructor Detail

Assert

public Assert()

Method Detail

assertionsEnabled

private static boolean assertionsEnabled()

assertEqualSort

public static void assertEqualSort(Sorted t1,
                                   Sorted t2)

Check whether two terms (or other sorted objects) are of the same sort.

Parameters:

t1 -

t2 -

assertSubSort

public static void assertSubSort(Sorted t1,
                                 Sorted t2)

Check whether the sort of t1 is a subsort of the sort of t2. I.e., check whether a substitution of t1 for t2 is legal.

Parameters:

t1 -

t2 -