-
Notifications
You must be signed in to change notification settings - Fork 56
Class DBC
Daniel Mittelman edited this page Apr 11, 2016
·
3 revisions
public enum DBC {
/*
* Utilities (55)
*/
static void require(boolean condition) throws Precondition;
static void require(boolean condition, String message) throws Precondition;
static void require(boolean condition, String format, Object[] args) throws Precondition;
static void require(boolean condition, String format, int n) throws Precondition;
static void require(boolean condition, String format, int n1, int n2) throws Precondition;
static void ensure(boolean condition) throws Postcondition;
static void ensure(boolean condition, String message) throws Postcondition;
static void ensure(boolean condition, String format, Object[] args) throws Postcondition;
static void ensure(boolean condition, String format, int n) throws Postcondition;
static void ensure(boolean condition, String format, int n1, int n2) throws Postcondition;
static void sure(boolean condition) throws Invariant;
static void sure(boolean condition, String message) throws Invariant;
static void sure(boolean condition, String format, Object[] args) throws Invariant;
static void sure(boolean condition, String format, int n) throws Invariant;
static void sure(boolean condition, String format, int n1, int n2) throws Invariant;
static void nonnull(Object o) throws NonNull;
static void nonnull(Object o, String message) throws NonNull;
static void nonnull(Object o, String format, Object[] args) throws NonNull;
static void positive(int n) throws Positive;
static void positive(double d) throws Positive;
static void positive(int n, String message) throws Positive;
static void positive(double d, String message) throws Positive;
static void positive(int n, String format, Object[] args) throws Positive;
static void positive(double d, String format, Object[] args) throws Positive;
static void negative(int n) throws Negative;
static void negative(double d) throws Negative;
static void negative(int n, String message) throws Negative;
static void negative(double d, String message) throws Negative;
static void negative(int n, String format, Object[] args) throws Negative;
static void negative(double d, String format, Object[] args) throws Negative;
static void nonnegative(int n) throws NonNegative;
static void nonnegative(double d) throws NonNegative;
static void nonnegative(int n, String message) throws NonNegative;
static void nonnegative(double d, String message) throws NonNegative;
static void nonnegative(int n, String format, Object[] args) throws NonNegative;
static void nonnegative(double d, String format, Object[] args) throws NonNegative;
static void nonpositive(int n) throws NonPositive;
static void nonpositive(double d) throws NonPositive;
static void nonpositive(int n, String message) throws NonPositive;
static void nonpositive(double d, String message) throws NonPositive;
static void nonpositive(int n, String format, Object[] args) throws NonPositive;
static void nonpositive(double d, String format, Object[] args) throws NonPositive;
static void unused(int _);
static void unused(double _);
static void unused(Object[] __);
static void unreachable() throws Reachability;
static void unreachable(String message) throws Reachability;
static void unreachable(String format, int n) throws Reachability;
static void unreachable(String format, int n1, int n2) throws Reachability;
static void unreachable(String format, Object[] args) throws Reachability;
static void unreachable(Exception e) throws Reachability;
static void checkInvariant(Checkable c);
static void warn(boolean condition, String s);
static void warn(String s);
static void todo(String[] args);
/*
* Nested types (3)
*/
abstract static interface Checkable { ... }
static final class Variant { ... }
abstract static class Bug extends RuntimeException { ... }
}Input types: Checkable, Exception.
Exception types: Invariant, Negative, NonNegative, NonNull, NonPositive, Positive, Postcondition, Precondition, Reachability.
public interface DBC.Checkable {
/*
* Type (1)
*/
void invariant();
}public static final class DBC.Variant {
/*
* Forge (1)
*/
Variant(int value) throws Initial;
/*
* Type (2)
*/
void check(int newValue) throws Nondecreasing, Underflow;
int value();
}Exception types: Initial, Nondecreasing, Underflow.
public abstract static class DBC.Bug extends RuntimeException {
/*
* Forge (2)
*/
Bug(String message);
Bug(Exception e);
/*
* Nested types (2)
*/
abstract static class Contract extends Bug { ... }
abstract static class Assertion extends Bug { ... }
}Input types: Exception.
public abstract static class DBC.Bug.Contract extends Bug {
/*
* Nested types (2)
*/
static final class Precondition extends Contract { ... }
static final class Postcondition extends Contract { ... }
}public static final class DBC.Bug.Contract.Precondition extends Contract {
/*
* Forge (3)
*/
Precondition();
Precondition(String message);
Precondition(String format, Object[] args);
}public static final class DBC.Bug.Contract.Postcondition extends Contract {
/*
* Forge (3)
*/
Postcondition();
Postcondition(String message);
Postcondition(String format, Object[] args);
}public abstract static class DBC.Bug.Assertion extends Bug {
/*
* Forge (2)
*/
Assertion(Exception e);
Assertion(String message);
/*
* Nested types (4)
*/
static final class Reachability extends Assertion { ... }
static final class Invariant extends Assertion { ... }
abstract static class Value extends Assertion { ... }
abstract static class Variant extends Assertion { ... }
}Input types: Exception.
public static final class DBC.Bug.Assertion.Reachability extends Assertion {
/*
* Forge (4)
*/
Reachability(String message);
Reachability(String[] args);
Reachability(String format, Object[] args);
Reachability(Exception e);
}Input types: Exception.
public static final class DBC.Bug.Assertion.Invariant extends Assertion {
/*
* Forge (3)
*/
Invariant();
Invariant(String message);
Invariant(String format, Object[] args);
}public abstract static class DBC.Bug.Assertion.Value extends Assertion {
/*
* Forge (3)
*/
Value();
Value(String message);
Value(String format, Object[] args);
/*
* Nested types (2)
*/
static final class NonNull extends Value { ... }
abstract static class Numerical extends Value { ... }
}public static final class DBC.Bug.Assertion.Value.NonNull extends Value {
/*
* Forge (3)
*/
NonNull();
NonNull(String message);
NonNull(String format, Object[] args);
}public abstract static class DBC.Bug.Assertion.Value.Numerical extends Value {
/*
* Forge (1)
*/
Numerical(String expected, double d, String message);
/*
* Nested types (4)
*/
static final class Positive extends Numerical { ... }
static final class Negative extends Numerical { ... }
static final class NonPositive extends Numerical { ... }
static final class NonNegative extends Numerical { ... }
}public static final class DBC.Bug.Assertion.Value.Numerical.Positive extends Numerical {
/*
* Forge (6)
*/
Positive(int n, String message);
Positive(double d, String message);
Positive(int n);
Positive(double d);
Positive(int n, String format, Object[] args);
Positive(double d, String format, Object[] args);
}public static final class DBC.Bug.Assertion.Value.Numerical.Negative extends Numerical {
/*
* Forge (6)
*/
Negative(int n, String message);
Negative(double d, String message);
Negative(int n);
Negative(double d);
Negative(int n, String format, Object[] args);
Negative(double d, String format, Object[] args);
}public static final class DBC.Bug.Assertion.Value.Numerical.NonPositive extends Numerical {
/*
* Forge (6)
*/
NonPositive(int n, String message);
NonPositive(double d, String message);
NonPositive(int n);
NonPositive(double d);
NonPositive(int n, String format, Object[] args);
NonPositive(double d, String format, Object[] args);
}public static final class DBC.Bug.Assertion.Value.Numerical.NonNegative extends Numerical {
/*
* Forge (6)
*/
NonNegative(int n, String message);
NonNegative(double d, String message);
NonNegative(int n);
NonNegative(double d);
NonNegative(int n, String format, Object[] args);
NonNegative(double d, String format, Object[] args);
}public abstract static class DBC.Bug.Assertion.Variant extends Assertion {
/*
* Forge (3)
*/
Variant(String message);
Variant(String format, int n);
Variant(String format, int n1, int n2);
/*
* Nested types (3)
*/
static final class Initial extends Variant { ... }
static final class Nondecreasing extends Variant { ... }
static final class Underflow extends Variant { ... }
}public static final class DBC.Bug.Assertion.Variant.Initial extends Variant {
/*
* Forge (1)
*/
Initial(int value);
}public static final class DBC.Bug.Assertion.Variant.Nondecreasing extends Variant {
/*
* Forge (1)
*/
Nondecreasing(int newValue, int oldValue);
}public static final class DBC.Bug.Assertion.Variant.Underflow extends Variant {
/*
* Forge (1)
*/
Underflow(int newValue);
}// SSDLPedia
package il.ac.technion.cs.ssdl.utils;
import static il.ac.technion.cs.ssdl.utils.Box.box;
import il.ac.technion.cs.ssdl.log.Log;
import il.ac.technion.cs.ssdl.stereotypes.Utility;
import il.ac.technion.cs.ssdl.strings.StringUtils;
import java.util.Formatter;
/**
* A simple implementation of design by contract services. Violations are
* reported to System.err. Error descriptions are passed by a
* printf like argument syntax. Services are often used with
* static import.
*
* Author: Yossi Gil (
* See: 11/01/2006)
*/
@Utility public enum DBC {
// A namespace: no values to this enum
;
/**
* A possibly non-returning method to be used for checking preconditions.
*
* condition if false, program will halt.
* Bug.Contract.Precondition A RuntimeException to be thrown
* in the case condition was
* false
*/
public static void require(final boolean condition) throws Bug.Contract.Precondition {
if (!condition)
throw new Bug.Contract.Precondition();
}
/**
* A possibly non-returning method to be used for checking preconditions. If
* the precondition fails, then a user supplied message is associated with
* the thrown exception.
*
* condition if false, program will halt.
* message text to be associated with the exception thrown in the
* case of an error.
* Bug.Contract.Precondition A RuntimeException to be thrown
* in the case condition was
* false
*/
public static void require(final boolean condition, final String message) throws Bug.Contract.Precondition {
if (!condition)
throw new Bug.Contract.Precondition(message);
}
/**
* A possibly non-returning method to be used for checking preconditions. If
* the precondition fails, then a user supplied formatted message (generated
* from printf like arguments) is associated with the thrown
* exception.
*
* condition if false, program will halt.
* format format string to be associated with the exception thrown in
* the case of an error.
* args printf-like arguments to be used with the format
* string.
* Bug.Contract.Precondition A RuntimeException to be thrown
* in the case condition was
* false
* @see #require(boolean, String, int)
* @see #require(boolean, String, int, int)
*/
public static void require(final boolean condition, final String format, final Object... args) throws Bug.Contract.Precondition {
if (!condition)
throw new Bug.Contract.Precondition(format, args);
}
/**
* A possibly non-returning method to be used for checking preconditions. If
* the precondition fails, then a user supplied formatted message (generated
* from one integer parameter) is associated with the thrown exception.
*
* condition if false, program will halt.
* format format string to be associated with the exception thrown in
* the case of an error.
* n an int to be passed to the format string
* Bug.Contract.Precondition A RuntimeException to be thrown
* in the case condition was
* false
* @see #require(boolean, String, int, int)
*/
public static void require(final boolean condition, final String format, final int n) throws Bug.Contract.Precondition {
if (!condition)
throw new Bug.Contract.Precondition(format, box(n));
}
/**
* A possibly non-returning method to be used for checking preconditions. If
* the precondition fails, then a user supplied formatted message (generated
* from two integer parameters) is associated with the thrown exception.
*
* condition if false, program will halt.
* format format string to be associated with the exception thrown in
* the case of an error.
* n1 the first int to be passed to the format
* string
* n2 the second int to be passed to the format
* string
* Bug.Contract.Precondition A RuntimeException to be thrown
* in the case condition was
* false
*/
public static void require(final boolean condition, final String format, final int n1, final int n2)
throws Bug.Contract.Precondition {
if (!condition)
throw new Bug.Contract.Precondition(format, box(n1), box(n2));
}
/**
* A possibly non-returning method to be used for checking postconditions.
*
* condition if false, program will halt.
* Bug.Contract.Postcondition A RuntimeException to be
* thrown in the case condition was
* false
*/
public static void ensure(final boolean condition) throws Bug.Contract.Postcondition {
if (!condition)
throw new Bug.Contract.Postcondition();
}
/**
* A possibly non-returning method to be used for checking postconditions.
* If the postcondition fails, then a user supplied message is associated
* with the thrown exception.
*
* condition if false, program will halt.
* message text to be associated with the exception thrown in the
* case of an error.
* Bug.Contract.Postcondition A RuntimeException to be
* thrown in the case condition was
* false
*/
public static void ensure(final boolean condition, final String message) throws Bug.Contract.Postcondition {
if (!condition)
throw new Bug.Contract.Precondition(message);
}
/**
* A possibly non-returning method to be used for checking postconditions.
* If the postcondition fails, then a user supplied formatted message
* (generated from printf like arguments) is associated with
* the thrown exception.
*
* condition if false, program will halt.
* format format string to be associated with the exception thrown in
* the case of an error.
* args printf-like arguments to be used with the format
* string.
* Bug.Contract.Postcondition A RuntimeException to be
* thrown in the case condition was
* false
* @see #ensure(boolean, String, int)
* @see #ensure(boolean, String, int, int)
*/
public static void ensure(final boolean condition, final String format, final Object... args) throws Bug.Contract.Postcondition {
if (!condition)
throw new Bug.Contract.Postcondition(format, args);
}
/**
* A possibly non-returning method to be used for checking postconditions.
* If the postcondition fails, then a user supplied formatted message
* (generated from one integer parameter) is associated with the thrown
* exception.
*
* condition if false, program will halt.
* format format string to be associated with the exception thrown in
* the case of an error.
* n an int to be passed to the format string
* Bug.Contract.Postcondition A RuntimeException to be
* thrown in the case condition was
* false
* @see #ensure(boolean, String, int, int)
*/
public static void ensure(final boolean condition, final String format, final int n) throws Bug.Contract.Postcondition {
if (!condition)
throw new Bug.Contract.Postcondition(format, box(n));
}
/**
* A possibly non-returning method to be used for checking postconditions.
* If the postcondition fails, then a user supplied formatted message
* (generated from two integer parameters) is associated with the thrown
* exception.
*
* condition if false, program will halt.
* format format string to be associated with the exception thrown in
* the case of an error.
* n1 the first int to be passed to the format
* string
* n2 the second int to be passed to the format
* string
* Bug.Contract.Postcondition A RuntimeException to be
* thrown in the case condition was
* false
*/
public static void ensure(final boolean condition, final String format, final int n1, final int n2)
throws Bug.Contract.Postcondition {
if (!condition)
throw new Bug.Contract.Postcondition(format, box(n1), box(n2));
}
/**
* A possibly non-returning method to be used for checking assertions.
*
* condition if false, program will halt.
* Bug.Assertion.Invariant A RuntimeException to be thrown
* in the case condition was
* false
*/
public static void sure(final boolean condition) throws Bug.Assertion.Invariant {
if (!condition)
throw new Bug.Assertion.Invariant();
}
/**
* A possibly non-returning method to be used for checking assertions. If
* the postcondition fails, then a user supplied message is associated with
* the thrown exception.
*
* condition if false, program will halt.
* message text to be associated with the exception thrown in the
* case of an error.
* Bug.Assertion.Invariant A RuntimeException to be thrown
* in the case condition was
* false
*/
public static void sure(final boolean condition, final String message) throws Bug.Assertion.Invariant {
if (!condition)
throw new Bug.Assertion.Invariant(message);
}
/**
* A possibly non-returning method to be used for checking assertions. If
* the postcondition fails, then a user supplied formatted message
* (generated from printf like arguments) is associated with
* the thrown exception.
*
* condition if false, program will halt.
* format format string to be associated with the exception thrown in
* the case of an error.
* args printf-like arguments to be used with the format
* string.
* Bug.Assertion.Invariant A RuntimeException to be thrown
* in the case condition was
* false
* @see #sure(boolean, String, int)
* @see #sure(boolean, String, int, int)
*/
public static void sure(final boolean condition, final String format, final Object... args) throws Bug.Assertion.Invariant {
if (!condition)
throw new Bug.Assertion.Invariant(format, args);
}
/**
* A possibly non-returning method to be used for checking assertions If the
* postcondition fails, then a user supplied formatted message (generated
* from one integer parameter) is associated with the thrown exception.
*
* condition if false, program will halt.
* format format string to be associated with the exception thrown in
* the case of an error.
* n an int to be passed to the format string
* Bug.Assertion.Invariant A RuntimeException to be thrown
* in the case condition was
* false
* @see #sure(boolean, String, int, int)
*/
public static void sure(final boolean condition, final String format, final int n) throws Bug.Assertion.Invariant {
if (!condition)
throw new Bug.Assertion.Invariant(format, box(n));
}
/**
* A possibly non-returning method to be used for checking assertions. If
* the postcondition fails, then a user supplied formatted message
* (generated from two integer parameters) is associated with the thrown
* exception.
*
* condition if false, program will halt.
* format format string to be associated with the exception thrown in
* the case of an error.
* n1 the first int to be passed to the format
* string
* n2 the second int to be passed to the format
* string
* Bug.Assertion.Invariant A RuntimeException to be thrown
* in the case condition was
* false
*/
public static void sure(final boolean condition, final String format, final int n1, final int n2)
throws Bug.Assertion.Invariant {
if (!condition)
throw new Bug.Assertion.Invariant(format, box(n1), box(n2));
}
/**
* A possibly non-returning method to be used for checking objects that
* should never be null.
*
* o if null, program will halt.
* Bug.Assertion.Value.NonNull in case o was
* null
*/
public static void nonnull(final Object o) throws Bug.Assertion.Value.NonNull {
if (o == null)
throw new Bug.Assertion.Value.NonNull();
}
/**
* A possibly non-returning method to be used for checking objects that
* should never be null.
*
* o if null, program will halt.
* message an error message to be associated with the failure
* Bug.Assertion.Value.NonNull in case o was
* null
*/
public static void nonnull(final Object o, final String message) throws Bug.Assertion.Value.NonNull {
if (o == null)
throw new Bug.Assertion.Value.NonNull(message);
}
/**
* A possibly non-returning method to be used for checking objects that
* should never be null.
*
* o if null, program will halt.
* format format string to be associated with the exception thrown in
* the case of an error.
* args printf-like arguments to be used with the format
* string.
* Bug.Assertion.Value.NonNull in case o was
* null
*/
public static void nonnull(final Object o, final String format, final Object... args) throws Bug.Assertion.Value.NonNull {
if (o == null)
throw new Bug.Assertion.Value.NonNull(format, args);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be positive.
*
* n a value which must be positive
* Bug.Assertion.Value.Numerical.Positive in case n was
* nonpositive
*/
public static void positive(final int n) throws Bug.Assertion.Value.Numerical.Positive {
if (n <= 0)
throw new Bug.Assertion.Value.Numerical.Positive(n);
}
/**
* A possibly non-returning method to be used for checking floating point
* numbers which must be positive.
*
* d a value which must be positive
* Bug.Assertion.Value.Numerical.Positive in case d was
* nonpositive
*/
public static void positive(final double d) throws Bug.Assertion.Value.Numerical.Positive {
if (d <= 0)
throw new Bug.Assertion.Value.Numerical.Positive(d);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be positive.
*
* n if negative program will halt.
* message text to be associated with the exception thrown in the
* case of an error.
* Bug.Assertion.Value.Numerical.Positive in case n was
* nonpositive
*/
public static void positive(final int n, final String message) throws Bug.Assertion.Value.Numerical.Positive {
if (n <= 0)
throw new Bug.Assertion.Value.Numerical.Positive(n, message);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be positive.
*
* d a value which must be positive
* message text to be associated with the exception thrown in the
* case of an error.
* Bug.Assertion.Value.Numerical.Positive in case n was
* nonpositive
*/
public static void positive(final double d, final String message) throws Bug.Assertion.Value.Numerical.Positive {
if (d <= 0)
throw new Bug.Assertion.Value.Numerical.Positive(d, message);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be negative.
*
* n a value which must be positive
* format format string to be associated with the exception thrown in
* the case of an error.
* args printf-like arguments to be used with the format
* string.
* Bug.Assertion.Value.Numerical.Positive in case d was
* nonpositive
*/
public static void positive(final int n, final String format, final Object... args)
throws Bug.Assertion.Value.Numerical.Positive {
if (n <= 0)
throw new Bug.Assertion.Value.Numerical.Positive(n, format, args);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be negative.
*
* d a value which must be positive
* format format string to be associated with the exception thrown in
* the case of an error.
* args printf-like arguments to be used with the format
* string.
* Bug.Assertion.Value.Numerical.Positive in case d was
* not positive
*/
public static void positive(final double d, final String format, final Object... args)
throws Bug.Assertion.Value.Numerical.Positive {
if (d <= 0)
throw new Bug.Assertion.Value.Numerical.Positive(d, format, args);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be negative.
*
* n a value which must be negative
* Bug.Assertion.Value.Numerical.Negative in case n was
* nonnegative
*/
public static void negative(final int n) throws Bug.Assertion.Value.Numerical.Negative {
if (n >= 0)
throw new Bug.Assertion.Value.Numerical.Negative(n);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be negative.
*
* d a value which must be negative
* Bug.Assertion.Value.Numerical.Negative in case d was
* nonnegative
*/
public static void negative(final double d) throws Bug.Assertion.Value.Numerical.Negative {
if (d >= 0)
throw new Bug.Assertion.Value.Numerical.Negative(d);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be negative.
*
* n a value which must be negative
* message text to be associated with the exception thrown in the
* case of an error.
* Bug.Assertion.Value.Numerical.Negative in case n was
* nonnegative
*/
public static void negative(final int n, final String message) throws Bug.Assertion.Value.Numerical.Negative {
if (n >= 0)
throw new Bug.Assertion.Value.Numerical.Negative(n, message);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be negative.
*
* d a value which must be negative
* message text to be associated with the exception thrown in the
* case of an error.
* Bug.Assertion.Value.Numerical.Negative in case d was
* nonnegative
*/
public static void negative(final double d, final String message) throws Bug.Assertion.Value.Numerical.Negative {
if (d >= 0)
throw new Bug.Assertion.Value.Numerical.Negative(d, message);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be negative.
*
* n a value which must be negative
* format format string to be associated with the exception thrown in
* the case of an error.
* args printf-like arguments to be used with the format
* string.
* Bug.Assertion.Value.Numerical.Negative in case n was
* nonnegative
*/
public static void negative(final int n, final String format, final Object... args)
throws Bug.Assertion.Value.Numerical.Negative {
if (n >= 0)
throw new Bug.Assertion.Value.Numerical.Negative(n, format, args);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be negative.
*
* d a value which must be negative
* format format string to be associated with the exception thrown in
* the case of an error.
* args printf-like arguments to be used with the format
* string.
* Bug.Assertion.Value.Numerical.Negative in case d was
* nonnegative
*/
public static void negative(final double d, final String format, final Object... args)
throws Bug.Assertion.Value.Numerical.Negative {
if (d >= 0)
throw new Bug.Assertion.Value.Numerical.Negative(d, format, args);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be nonnegative.
*
* n a value which must be nonnegative
* Bug.Assertion.Value.Numerical.NonNegative in case n
* was negative
*/
public static void nonnegative(final int n) throws Bug.Assertion.Value.Numerical.NonNegative {
if (n < 0)
throw new Bug.Assertion.Value.Numerical.NonNegative(n);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be nonnegative.
*
* d a value which must be nonnegative
* Bug.Assertion.Value.Numerical.NonNegative in case d
* was negative
*/
public static void nonnegative(final double d) throws Bug.Assertion.Value.Numerical.NonNegative {
if (d < 0)
throw new Bug.Assertion.Value.Numerical.NonNegative(d);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be nonnegative.
*
* n a value which must be nonnegative
* message text to be associated with the exception thrown in the
* case of an error.
* Bug.Assertion.Value.Numerical.NonNegative in case n
* was negative
*/
public static void nonnegative(final int n, final String message) throws Bug.Assertion.Value.Numerical.NonNegative {
if (n < 0)
throw new Bug.Assertion.Value.Numerical.NonNegative(n, message);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be nonnegative.
*
* d a value which must be nonnegative
* message text to be associated with the exception thrown in the
* case of an error.
* Bug.Assertion.Value.Numerical.NonNegative in case n
* was negative
*/
public static void nonnegative(final double d, final String message) throws Bug.Assertion.Value.Numerical.NonNegative {
if (d < 0)
throw new Bug.Assertion.Value.Numerical.NonNegative(d, message);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be nonnegative.
*
* n a value which must be nonnegative
* format format string to be associated with the exception thrown in
* the case of an error.
* args printf-like arguments to be used with the format
* string.
* Bug.Assertion.Value.Numerical.NonNegative in case n
* was negative
*/
public static void nonnegative(final int n, final String format, final Object... args)
throws Bug.Assertion.Value.Numerical.NonNegative {
if (n < 0)
throw new Bug.Assertion.Value.Numerical.NonNegative(n, format, args);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be nonnegative.
*
* d a value which must be nonnegative
* format format string to be associated with the exception thrown in
* the case of an error.
* args printf-like arguments to be used with the format
* string.
* Bug.Assertion.Value.Numerical.NonNegative in case d
* was negative
*/
public static void nonnegative(final double d, final String format, final Object... args)
throws Bug.Assertion.Value.Numerical.NonNegative {
if (d < 0)
throw new Bug.Assertion.Value.Numerical.NonNegative(d, format, args);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be nonpositive.
*
* n a value which must be nonpositive
* Bug.Assertion.Value.Numerical.NonPositive in case n
* was positive
*/
public static void nonpositive(final int n) throws Bug.Assertion.Value.Numerical.NonPositive {
if (n > 0)
throw new Bug.Assertion.Value.Numerical.NonPositive(n);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be nonpositive.
*
* d a value which must be nonpositive
* Bug.Assertion.Value.Numerical.NonPositive in case d
* was positive
*/
public static void nonpositive(final double d) throws Bug.Assertion.Value.Numerical.NonPositive {
if (d > 0)
throw new Bug.Assertion.Value.Numerical.NonPositive(d);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be nonpositive.
*
* n a value which must be nonpositive
* message text to be associated with the exception thrown in the
* case of an error.
* Bug.Assertion.Value.Numerical.NonPositive in case n
* was positive
*/
public static void nonpositive(final int n, final String message) throws Bug.Assertion.Value.Numerical.NonPositive {
if (n > 0)
throw new Bug.Assertion.Value.Numerical.NonPositive(n, message);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be nonpositive.
*
* d a value which must be nonpositive
* message text to be associated with the exception thrown in the
* case of an error.
* Bug.Assertion.Value.Numerical.NonPositive in case d
* was positive
*/
public static void nonpositive(final double d, final String message) throws Bug.Assertion.Value.Numerical.NonPositive {
if (d > 0)
throw new Bug.Assertion.Value.Numerical.NonPositive(d, message);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be nonpositive.
*
* n a value which must be nonpositive
* format format string to be associated with the exception thrown in
* the case of an error.
* args printf-like arguments to be used with the format
* string.
* Bug.Assertion.Value.Numerical.NonPositive in case n
* was positive
*/
public static void nonpositive(final int n, final String format, final Object... args)
throws Bug.Assertion.Value.Numerical.NonPositive {
if (n > 0)
throw new Bug.Assertion.Value.Numerical.NonPositive(n, format, args);
}
/**
* A possibly non-returning method to be used for checking integers which
* must be nonpositive.
*
* d a value which must be nonpositive
* format format string to be associated with the exception thrown in
* the case of an error.
* args printf-like arguments to be used with the format
* string.
* Bug.Assertion.Value.Numerical.NonPositive in case d
* was positive
*/
public static void nonpositive(final double d, final String format, final Object... args)
throws Bug.Assertion.Value.Numerical.NonPositive {
if (d > 0)
throw new Bug.Assertion.Value.Numerical.NonPositive(d, format, args);
}
/**
* A do nothing method to document the fact that an int
* parameter (or local variable) is not used by a function, and to suppress
* the warning.
*
* _ the unused parameter
*/
public static void unused(@SuppressWarnings("unused") final int _) {
// empty
}
/**
* A do nothing method to document the fact that adouble
* parameter (or local variable) is not used by a function, and to suppress
* the warning.
*
* _ the unused parameter
*/
public static void unused(@SuppressWarnings("unused") final double _) {
// empty
}
/**
* A do nothing method to document the fact that some Object(s)
* parameter(s) (or local variable(s)) are not used by a function. Calling
* this method saves the caller the trouble of suppressing a "variable
* unused" warnings on the argument(s).
*
* __ the unused parameters
*/
public static void unused(@SuppressWarnings("unused") final Object... __) {
// Empty
}
/**
* A never-returning method to be used in points of code which should never
* be reached.
*
* Bug.Assertion.Reachability will always be thrown
*/
public static void unreachable() throws Bug.Assertion.Reachability {
throw new Bug.Assertion.Reachability("");
}
/**
* A never-returning method to be used in points of code which should never
* be reached.
*
* message a string describing the violation
* Bug.Assertion.Reachability will always be thrown
*/
public static void unreachable(final String message) throws Bug.Assertion.Reachability {
throw new Bug.Assertion.Reachability(message);
}
/**
* A never-returning method to be used in points of code which should never
* be reached.
*
* format format string to be associated with the exception thrown in
* the case of an error.
* n an int to be passed to the format string
* Bug.Assertion.Reachability will always be thrown
*/
public static void unreachable(final String format, final int n) throws Bug.Assertion.Reachability {
throw new Bug.Assertion.Reachability(StringUtils.sprintf(format, box(n)));
}
/**
* A never-returning method to be used in points of code which should never
* be reached.
*
* format format string to be associated with the exception thrown in
* the case of an error.
* n1 the first int to be passed to the format
* string
* n2 the second int to be passed to the format
* string
* Bug.Assertion.Reachability will always be thrown
*/
public static void unreachable(final String format, final int n1, final int n2) throws Bug.Assertion.Reachability {
throw new Bug.Assertion.Reachability(StringUtils.sprintf(format, box(n1), box(n2)));
}
public static void unreachable(final String format, final Object... args) throws Bug.Assertion.Reachability {
throw new Bug.Assertion.Reachability(StringUtils.sprintf(format, args));
}
/**
* A never-returning method intended for use in catch blocks around code
* whose declared exception will never be thrown (unless for bugs).
*
* e an exception describing
* Bug.Assertion.Reachability will always be thrown
*/
public static void unreachable(final Exception e) throws Bug.Assertion.Reachability {
throw new Bug.Assertion.Reachability(e);
}
/**
* Exercise the Checkable#invariant()
*
* c a checkable object whose invariant should be checked
*/
public static void checkInvariant(final Checkable c) {
c.toString();
c.invariant();
}
public static void warn(final boolean condition, final String s) {
if (condition)
return;
warn(s);
}
public static void warn(final String s) {
System.out.println(s);
}
/**
* A never-returning method indicating code sites with missing functionality
*
* args a list of strings in a printf like format
* describing the task to be done.
*/
public static void todo(final String... args) {
error("Feature unsupported. ", args);
}
/**
* A possibly non returning method used in class implementation.
*
* cond If false, method will not return and
* print error message.
* kind A string describing an error kind, e.g., pre-condition
* failure
* args Additional strings describing an error kind in a
* printf format.
*/
static void error(final boolean cond, final String kind, final String... args) {
if (cond)
return;
error(kind, args);
}
private static void error(final String kind, final String... args) {
final String s = buildMessage(kind, args);
System.out.flush();
System.err.flush();
System.err.println(s);
System.err.flush();
Log.printStackTrace();
STOP.stop(s);
}
private static String buildMessage(final String kind, final String... args) {
String $ = kind + " ";
switch (args.length) {
case 0:
break;
case 1:
$ += args[0];
break;
default:
final Object os[] = new Object[args.length - 1];
for (int i = 1; i < args.length; i++)
os[i - 1] = args[i];
final Formatter f = new Formatter();
f.format(args[0], os);
$ += f.out();
}
return $;
}
/**
* An interface representing a class with an invariant.
*
* Author: Yossi Gil
* See: 11/04/2006
*/
public static interface Checkable {
/**
* This function represents the invariant of the implementing class. It
* returns nothing. However, if the invariant is violated, a runtime
* exception aborts execution.
*/
void invariant();
}
/**
* A class to emulate Eiffel's variant construct. To use,
* create an object of this type, initializing it with the variant's first
* value , and then call function #check(int) successively.
*
* Author: Yossi Gil
* See: 05/06/2007
*/
public static final class Variant {
private int value;
/**
* Initialize a variant, with a specified value
*
* value a non-negative value
* Bug.Assertion.Variant.Initial in case initial value is
* negative
*/
public Variant(final int value) throws Bug.Assertion.Variant.Initial {
if (value < 0)
throw new Bug.Assertion.Variant.Initial(value);
this.value = value;
}
/**
* reset the variant value to a new, smaller value value; abort if the
* new value is negative or no lesser than the previous value.
*
* newValue the next value of this variant.
* Bug.Assertion.Variant.Nondecreasing in case the variant's
* value did not decrease
* Bug.Assertion.Variant.Underflow in case the variant's value
* went negative
*/
public void check(final int newValue) throws Bug.Assertion.Variant.Nondecreasing, Bug.Assertion.Variant.Underflow {
if (newValue >= value)
throw new Bug.Assertion.Variant.Nondecreasing(newValue, value);
if (newValue < 0)
throw new Bug.Assertion.Variant.Underflow(newValue);
value = newValue;
}
/**
* inspect the variant's value.
*
* Return: a non-negative integer which is the current value of this
* object
*/
public int value() {
return value;
}
}
/**
* The base of all exception classes thrown as a result of violations of
* contracts, assertions, and the such. This class derives from
* RuntimeException since errors of this sort are programming-, not
* runtime- errors. Programming errors cannot be corrected at runtime, and
* hence all errors of this class and its descendants should not be caught
* by ordinary applications.
*
* Author: Yossi Gil, the Technion.
* See: 04/08/2008
*/
public abstract static class Bug extends RuntimeException {
/**
* instantiate this class with a given textual description
*
* message a description of the exceptional situation
*/
public Bug(final String message) {
super(message);
}
/**
* convert an ordinary exception into this type.
*
* e the exception to convert
*/
public Bug(final Exception e) {
super(e);
}
/**
* Abstract base class of contract (pre- and post-condition) violations
*
* Author: Yossi Gil, the Technion.
* See: 04/08/2008
*/
public abstract static class Contract extends Bug {
/**
* args
*/
protected Contract(final String... args) {
super(StringUtils.sprintf(args));
}
private static final long serialVersionUID = -8228321063991272253L;
/**
* Thrown in case a pre-condition was not satisfied
*
* Author: Yossi Gil, the Technion.
* See: 04/08/2008
*/
public static final class Precondition extends Contract {
/**
* instantiate this class with no textual description
*/
public Precondition() {
super("");
}
/**
* instantiate this class with a given textual description
*
* message a description of the exceptional situation
*/
public Precondition(final String message) {
super(StringUtils.sprintf(message));
}
public Precondition(final String format, final Object... args) {
super(StringUtils.sprintf(format, args));
}
private static final long serialVersionUID = -5317027949287654746L;
}
/**
* Thrown in case a post-condition was not satisfied
*
* Author: Yossi Gil, the Technion.
* See: 04/08/2008
*/
public static final class Postcondition extends Contract {
/**
* instantiate this class with no textual description
*/
public Postcondition() {
super("");
}
/**
* instantiate this class with a given textual description
*
* message a description of the exceptional situation
*/
public Postcondition(final String message) {
super(StringUtils.sprintf(message));
}
public Postcondition(final String format, final Object... args) {
super(StringUtils.sprintf(format, args));
}
private static final long serialVersionUID = -3177288122092390767L;
}
}
private static final long serialVersionUID = 8737036163937047206L;
/**
* This is the root of all assertion related exceptions, including
* contract violations.
*
* Author: Yossi Gil, the Technion.
* See: 04/08/2008
*/
public abstract static class Assertion extends Bug {
/**
* convert an ordinary exception into this kind.
*
* e the exception to convert
*/
public Assertion(final Exception e) {
super(e);
}
/**
* instantiate this class with a given textual description
*
* message a description of the exceptional situation
*/
public Assertion(final String message) {
super(message);
}
/**
* Thrown in case execution reached code that should never be
* executed
*
* Author: Yossi Gil, the Technion.
* See: 04/08/2008
*/
public static final class Reachability extends Assertion {
/**
* instantiate this class with a given textual description
*
* message a description of the exceptional situation
*/
public Reachability(final String message) {
super(message);
}
/**
* Create a new instance, with a message composed by a format
* and a string
*
* args the arguments making the message in a
* printf like format
*/
public Reachability(final String... args) {
super(StringUtils.sprintf(args));
}
public Reachability(final String format, final Object[] args) {
super(StringUtils.sprintf(format, args));
}
/**
* Convert an arbitrary exception to this type
*
* e the exception to convert
*/
public Reachability(final Exception e) {
super(e);
}
private static final long serialVersionUID = -1522565621962121759L;
}
private static final long serialVersionUID = -7893002781575729383L;
/**
* Thrown in case a class invariant was violated.
*
* Author: Yossi Gil, the Technion.
* See: 04/08/2008
*/
public static final class Invariant extends Assertion {
/**
* instantiate this class with no textual description
*/
public Invariant() {
super("");
}
/**
* instantiate this class with a given textual description
*
* message a description of the exceptional situation
*/
public Invariant(final String message) {
super(StringUtils.sprintf(message));
}
public Invariant(final String format, final Object... args) {
super(StringUtils.sprintf(format, args));
}
private static final long serialVersionUID = 3613179176640712216L;
}
/**
* Abstract base class of all exceptions thrown in case a value
* violated a condition placed on it.
*
* Author: Yossi Gil, the Technion.
* See: 04/08/2008
*/
public abstract static class Value extends Assertion {
/**
* instantiate this class with no textual description
*/
public Value() {
super("");
}
/**
* instantiate this class with a given textual description
*
* message a description of the exceptional situation
*/
public Value(final String message) {
super(message);
}
public Value(final String format, final Object... args) {
super(StringUtils.sprintf(format, args));
}
private static final long serialVersionUID = -5932674935888850461L;
/**
* Thrown in case a value was null, when it
* was expected to be non-code>null</tt>.
*
* Author: Yossi Gil
* See: 18/01/2008
*/
public static final class NonNull extends Value {
/**
* instantiate this class with no textual description
*/
public NonNull() {
super();
}
/**
* instantiate this class with a given textual description
*
* message a description of the exceptional situation
*/
public NonNull(final String message) {
super(message);
}
public NonNull(final String format, final Object... args) {
super(format, args);
}
private static final long serialVersionUID = -6739260930609363921L;
}
/**
* Abstract base class of exceptions thrown when a numerical
* value did not satisfy conditions assumed on it.
*
* Author: Yossi Gil, the Technion.
* See: 04/08/2008
*/
public abstract static class Numerical extends Value {
Numerical(final String expected, final int n, final String message) {
super(StringUtils.sprintf("Found %d while expecting a %s integer. ", box(n), expected) + message);
}
public Numerical(final String expected, final double d, final String message) {
super(StringUtils.sprintf("Found %g while expecting a %s number. ", box(d), expected) + message);
}
private static final long serialVersionUID = 6004150110997223579L;
/**
* Thrown when a numerical value assumed to be positive, was
* not.
*
* Author: Yossi Gil
* See: 23/01/2008
*/
public static final class Positive extends Numerical {
static final String expected = "positive";
public Positive(final int n, final String message) {
super(expected, n, message);
}
public Positive(final double d, final String message) {
super(expected, d, message);
}
public Positive(final int n) {
this(n, "");
}
public Positive(final double d) {
this(d, "");
}
public Positive(final int n, final String format, final Object... args) {
this(n, StringUtils.sprintf(format, args));
}
public Positive(final double d, final String format, final Object... args) {
this(d, StringUtils.sprintf(format, args));
}
private static final long serialVersionUID = -5312054045684211451L;
}
/**
* Thrown when a numerical value assumed to be negative, was
* not.
*
* Author: Yossi Gil
* See: 23/01/2008
*/
public static final class Negative extends Numerical {
static final String expected = "neative";
public Negative(final int n, final String message) {
super(expected, n, message);
}
public Negative(final double d, final String message) {
super(expected, d, message);
}
public Negative(final int n) {
this(n, "");
}
public Negative(final double d) {
this(d, "");
}
public Negative(final int n, final String format, final Object... args) {
this(n, StringUtils.sprintf(format, args));
}
public Negative(final double d, final String format, final Object... args) {
this(d, StringUtils.sprintf(format, args));
}
private static final long serialVersionUID = 4550076451966877958L;
}
/**
* Author: Yossi Gil
* See: 23/01/2008
*/
public static final class NonPositive extends Numerical {
static final String expected = "nonpositive";
public NonPositive(final int n, final String message) {
super("nonpositive", n, message);
}
public NonPositive(final double d, final String message) {
super("nonpositive", d, message);
}
public NonPositive(final int n) {
this(n, "");
}
public NonPositive(final double d) {
this(d, "");
}
public NonPositive(final int n, final String format, final Object... args) {
this(n, StringUtils.sprintf(format, args));
}
public NonPositive(final double d, final String format, final Object... args) {
this(d, StringUtils.sprintf(format, args));
}
private static final long serialVersionUID = -8815781684971495019L;
}
/**
* Thrown when a numerical value assumed to be non-negative,
* was not.
*
* Author: Yossi Gil
* See: 23/01/2008
*/
public static final class NonNegative extends Numerical {
static final String expected = "nonnegative";
public NonNegative(final int n, final String message) {
super("expected", n, message);
}
public NonNegative(final double d, final String message) {
super("expected", d, message);
}
public NonNegative(final int n) {
this(n, "");
}
public NonNegative(final double d) {
this(d, "");
}
public NonNegative(final int n, final String format, final Object... args) {
this(n, StringUtils.sprintf(format, args));
}
public NonNegative(final double d, final String format, final Object... args) {
this(d, StringUtils.sprintf(format, args));
}
private static final long serialVersionUID = 1L;
}
}
}
/**
* Abstract base class of exceptions thrown when a loop variant
* failed.
*
* Author: Yossi Gil, the Technion.
* See: 04/08/2008
*/
public abstract static class Variant extends Assertion {
/**
* instantiate this class with a given textual description
*
* message a description of the exceptional situation
*/
public Variant(final String message) {
super(message);
}
public Variant(final String format, final int n) {
this(StringUtils.sprintf(format, "" + n));
}
public Variant(final String format, final int n1, final int n2) {
this(StringUtils.sprintf(format, "" + n1, "" + n2));
}
/**
*Thrown when the initial value of a loop variant was negative.
*
* Author: Yossi Gil, the Technion.
* See: 04/08/2008
*/
public static final class Initial extends Variant {
public Initial(final int value) {
super("Initial variant value (%d) is negative", value);
}
private static final long serialVersionUID = -6719831484164226074L;
}
/**
* Thrown if an iteration of a certain loop failed to decrease
* this loop's variant.
*
* Author: Yossi Gil, the Technion.
* See: 04/08/2008
*/
public static final class Nondecreasing extends Variant {
public Nondecreasing(final int newValue, final int oldValue) {
super("New variant value (%d) should be less than previous value (%d)", newValue, oldValue);
}
private static final long serialVersionUID = 5006328864309542167L;
}
private static final long serialVersionUID = 5055379624378837959L;
/**
* Thrown if an iteration of a certain loop tried to make this
* loop's variant negative.
*
* Author: Yossi Gil, the Technion.
* See: 04/08/2008
*/
public static final class Underflow extends Variant {
public Underflow(final int newValue) {
super("New variant value (%d) is negative", newValue);
}
private static final long serialVersionUID = 8362864540539118946L;
}
}
}
}
}| Metric | Value | Acronym | Explanation |
|---|---|---|---|
| LOC | 1470 | Lines Of Code | Total number of lines in the code |
| SCC | 168 | SemiColons Count | Total number of semicolon tokens found in the code. |
| NOT | 4329 | Number Of Tokens | Comments, whitespace and text which cannot be made into a token not included. |
| VCC | 38247 | Visible Characters Count | The total number of non-white (i.e., not space, tab, newline, carriage return, form feed) characters. |
| CCC | 15902 | Code Characters Count | Total number of non-white characters in tokens. White space characters in string and character literals are not counted. |
| UIC | 94 | Unique Identifiers Count | The number of different identifiers found in the code |
| WHC | 11 | Weighted Horizontal Complexity | A heuritistic on horizontal complexity |
| Statistic | Value |
|---|---|
| Average token length | 3.7 |
| Tokens/line | 2.9 |
| Visible characters/line | 26 |
| Code characters/line | 11 |
| Semicolons/tokens | 3% |
| Comment text percentage | 58% |
| Token Kind | Occurrences |
|---|---|
| KEYWORD | 995 |
| OPERATOR | 97 |
| LITERAL | 85 |
| ID | 1335 |
| PUNCTUATION | 1817 |
| COMMENT | 102 |
| OTHER | 2210 |