jass.modern
Annotation Type SpecCase


@Documented
@Retention(value=CLASS)
@Target(value={METHOD,CONSTRUCTOR})
public @interface SpecCase

The SpecCase-annotation can be used to specify the behaviour of a method or constructor. The definition of a specification case consists at most of three parts:

  1. pre(): The pre-condition of the method.
  2. post(): A post-condition which must hold, if the method returns normally (e.g. not throwing an exception)
  3. signalsPost(): A post-condition which must hold, if the method returns throwing an exeception (see signals()).
In addition, preMsg(), postMsg(), and signalsMsg() allows to link a custom message to a condition. If a condition does not hold, the accordant message is used as error message.
The visibility()-attribute can be used to set the visiblity of the specification. Two things are important when it comes to visibility:
  1. Visibility can not be larger (more public) than the visibility of its target
  2. Elements referenced by contract must have the same or a less strict visibility. E.g. a public spec can not rely on private members:
     class CU {
      private int value;
      
      @SpecCase(pre="value == 5", visibility=PUBLIC)
      public void m(){
            //...
      }
     }
     
    Above code will result in an compile error because the visibility of value and the SpecCase collide.


Optional Element Summary
 String post
          The post-condition of the spec-case.
 String postMsg
          An error message in case the post-condition does not hold.
 String pre
          The pre-condition of the spec-case.
 String preMsg
          An error message in case the pre-condition does not hold.
 Class<? extends Exception> signals
           
 String signalsMsg
          An error message in case the exceptional post-condition does not hold.
 String signalsPost
          The post-condition of the spec-case in case the target (method or constructor) terminates with an exception.
 Visibility visibility
           
 

pre

@Code(translator={jass.modern.core.compile.transform.ModelVariableTransformer.class,jass.modern.core.compile.transform.QuantifierTransformer.class})
public abstract String pre
The pre-condition of the spec-case. Must be valid Java code which evaluates to a boolean! The default value is the empty string.

Returns:
Default:
""

preMsg

public abstract String preMsg
An error message in case the pre-condition does not hold.

Returns:
The pre-condition error message.
Default:
""

post

@Code(translator={jass.modern.core.compile.transform.ReturnTransformer.class,jass.modern.core.compile.transform.ModelVariableTransformer.class,jass.modern.core.compile.transform.OldTransformer.class,jass.modern.core.compile.transform.QuantifierTransformer.class})
public abstract String post
The post-condition of the spec-case. Must be valid Java code which evaluates to a boolean! The default value is the empty string.

Returns:
Default:
""

postMsg

public abstract String postMsg
An error message in case the post-condition does not hold.

Returns:
The post-condition error message.
Default:
""

signals

public abstract Class<? extends Exception> signals
Returns:
Default:
java.lang.Exception.class

signalsPost

@Code(translator={jass.modern.core.compile.transform.SignalsTransformer.class,jass.modern.core.compile.transform.ModelVariableTransformer.class,jass.modern.core.compile.transform.OldTransformer.class,jass.modern.core.compile.transform.QuantifierTransformer.class})
public abstract String signalsPost
The post-condition of the spec-case in case the target (method or constructor) terminates with an exception. Must be valid Java code which evaluates to a boolean! The default value is the empty string.

Returns:
Default:
""

signalsMsg

public abstract String signalsMsg
An error message in case the exceptional post-condition does not hold.

Returns:
The exceptional post-condition.
Default:
""

visibility

public abstract Visibility visibility
Returns:
The visibility of this method specification.
Default:
jass.modern.Visibility.TARGET