Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: REQUIRED | OPTIONAL DETAIL: ELEMENT

org.jmlspecs.annotation
Annotation Type SpecCase

@Retention(value=RUNTIME)
@Documented
public @interface SpecCase

Optional Element Summary
 java.lang.String accessible
           
 java.lang.String accessibleRedundantly
           
 java.lang.String assignable
           
 java.lang.String assignableRedundantly
           
 java.lang.String callable
           
 java.lang.String callableRedundantly
           
 java.lang.String captures
           
 java.lang.String capturesRedundantly
           
 java.lang.String diverges
           
 java.lang.String divergesRedundantly
           
 java.lang.String duration
           
 java.lang.String durationRedundantly
           
 java.lang.String ensures
           
 java.lang.String ensuresRedundantly
           
 java.lang.String forall
           
 java.lang.String header
           
 java.lang.String measuredBy
           
 java.lang.String measuredByRedundantly
           
 java.lang.String modelProgram
           
 java.lang.String old
           
 java.lang.String requires
           
 java.lang.String requiresRedundantly
           
 java.lang.String signals
           
 java.lang.String signalsOnly
           
 java.lang.String signalsOnlyRedundantly
           
 java.lang.String signalsRedundantly
           
 java.lang.String tag
          tag format: (('+'|'-')? JavaId) (',' ('+'|'-') JavaId)*)?
 java.lang.String when
           
 java.lang.String whenRedundantly
           
 java.lang.String workingSpace
           
 java.lang.String workingSpaceRedundantly
           
 

tag

public abstract java.lang.String tag
tag format: (('+'|'-')? JavaId) (',' ('+'|'-') JavaId)*)?

Default:
""

header

public abstract java.lang.String header
Default:
""

forall

public abstract java.lang.String forall
Default:
"$not_specified"

old

public abstract java.lang.String old
Default:
"$not_specified"

requires

public abstract java.lang.String requires
Default:
"$not_specified"

requiresRedundantly

public abstract java.lang.String requiresRedundantly
Default:
"$not_specified"

ensures

public abstract java.lang.String ensures
Default:
"$not_specified"

ensuresRedundantly

public abstract java.lang.String ensuresRedundantly
Default:
"$not_specified"

signals

public abstract java.lang.String signals
Default:
"$not_specified"

signalsRedundantly

public abstract java.lang.String signalsRedundantly
Default:
"$not_specified"

signalsOnly

public abstract java.lang.String signalsOnly
Default:
"$not_specified"

signalsOnlyRedundantly

public abstract java.lang.String signalsOnlyRedundantly
Default:
"$not_specified"

diverges

public abstract java.lang.String diverges
Default:
"$not_specified"

divergesRedundantly

public abstract java.lang.String divergesRedundantly
Default:
"$not_specified"

when

public abstract java.lang.String when
Default:
"$not_specified"

whenRedundantly

public abstract java.lang.String whenRedundantly
Default:
"$not_specified"

assignable

public abstract java.lang.String assignable
Default:
"$not_specified"

assignableRedundantly

public abstract java.lang.String assignableRedundantly
Default:
"$not_specified"

accessible

public abstract java.lang.String accessible
Default:
"$not_specified"

accessibleRedundantly

public abstract java.lang.String accessibleRedundantly
Default:
"$not_specified"

callable

public abstract java.lang.String callable
Default:
"$not_specified"

callableRedundantly

public abstract java.lang.String callableRedundantly
Default:
"$not_specified"

measuredBy

public abstract java.lang.String measuredBy
Default:
"$not_specified"

measuredByRedundantly

public abstract java.lang.String measuredByRedundantly
Default:
"$not_specified"

captures

public abstract java.lang.String captures
Default:
"$not_specified"

capturesRedundantly

public abstract java.lang.String capturesRedundantly
Default:
"$not_specified"

workingSpace

public abstract java.lang.String workingSpace
Default:
"$not_specified"

workingSpaceRedundantly

public abstract java.lang.String workingSpaceRedundantly
Default:
"$not_specified"

duration

public abstract java.lang.String duration
Default:
"$not_specified"

durationRedundantly

public abstract java.lang.String durationRedundantly
Default:
"$not_specified"

modelProgram

public abstract java.lang.String modelProgram
Default:
"$not_specified"
Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: REQUIRED | OPTIONAL DETAIL: ELEMENT