A taste of things to come

Now to make it work!

/**
 * Marks a method with a <em>pre-condition</em>.  The required annotation
 * {@link #value()} is a <code>boolean</code> condition.  The optional
 * {@link #message()} is used in {@link DBCException} if the condition
 * fails.
 */
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.METHOD)
public @interface pre {
    boolean value();

    String message() default "";
}

/**
 * Marks a method with a <em>post-condition</em>.  The required annotation
 * {@link #value()} is a <code>boolean</code> condition.  The optional
 * {@link #message()} is used in {@link DBCException} if the condition
 * fails.
 */
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.METHOD)
public @interface post {
    boolean value();

    String message() default "";
}

/**
 * Marks a method with an <em>invariant</em>.  The required annotation
 * {@link #value()} is a <code>boolean</code> invariant.  The optional
 * {@link #message()} is used in {@link DBCException} if the invariant
 * fails.
 */
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.METHOD)
public @interface inv {
    boolean value();

    String message() default "";
}

UPDATE: I'll have to think about this longer. Turns out that annotations only accept constants or expressions which evaluate to constants. A constant pre-condition isn't very interesting.