|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: REQUIRED | OPTIONAL | DETAIL: ELEMENT |
@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:
pre()
: The pre-condition of the method.
post()
: A post-condition which must hold, if
the method returns normally (e.g. not throwing an exception)
signalsPost()
: A post-condition which must hold,
if the method returns throwing an exeception (see signals()
).
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.
visibility()
-attribute can be used to set the
visiblity of the specification. Two things are important when it comes
to visibility:
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
|
@Code(translator={jass.modern.core.compile.transform.ModelVariableTransformer.class,jass.modern.core.compile.transform.QuantifierTransformer.class}) public abstract String pre
empty string
.
public abstract String preMsg
@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
empty string
.
public abstract String postMsg
public abstract Class<? extends Exception> signals
@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
empty string
.
public abstract String signalsMsg
public abstract Visibility visibility
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: REQUIRED | OPTIONAL | DETAIL: ELEMENT |