private static class SpecificationInjector.JMLFactory extends Object
Modifier and Type | Field and Description |
---|---|
private static String |
BY |
private static String |
DEFAULT_INDENTATION |
private static String |
DEFAULT_KEY |
private static String |
DETERMINES |
private String |
indentation |
private static String |
JML_CLAUSE_END |
private static String |
JML_END |
private static String |
JML_LINE_START |
private static String |
JML_START |
private Map<String,Set<Map.Entry<String,SpecificationEntity.Type>>> |
respects |
private static String |
RESULT |
private SpecificationContainer |
sc |
Constructor and Description |
---|
SpecificationInjector.JMLFactory(int indent) |
SpecificationInjector.JMLFactory(SpecificationContainer sc) |
Modifier and Type | Method and Description |
---|---|
(package private) void |
addResultToDetermines(SpecificationEntity.Type t) |
(package private) void |
addResultToDetermines(String key,
SpecificationEntity.Type t)
Adds \result to a determines clause labeled by key.
|
(package private) void |
addToDetermines(String name,
SpecificationEntity.Type t) |
(package private) void |
addToDetermines(String name,
SpecificationEntity.Type t,
String key) |
(package private) String |
getRespects(Set<Map.Entry<String,SpecificationEntity.Type>> oneRespect,
SpecificationEntity.Type t) |
(package private) String |
getRespects(Set<String> oneRespect) |
(package private) String |
getRespects(String domain,
SpecificationEntity.Type t) |
(package private) String |
getSpecification()
Gets a formatted JML comment.
|
private void |
put(String key,
Map.Entry<String,SpecificationEntity.Type> value) |
private void |
put(String key,
SpecificationEntity.Type t,
String value) |
private static final String DEFAULT_INDENTATION
private static final String DEFAULT_KEY
private static final String RESULT
private static final String DETERMINES
private static final String BY
private static final String JML_LINE_START
private static final String JML_END
private static final String JML_CLAUSE_END
private static final String JML_START
private final String indentation
private SpecificationContainer sc
SpecificationInjector.JMLFactory(SpecificationContainer sc)
SpecificationInjector.JMLFactory(int indent)
void addResultToDetermines(SpecificationEntity.Type t)
void addResultToDetermines(String key, SpecificationEntity.Type t)
void addToDetermines(String name, SpecificationEntity.Type t)
void addToDetermines(String name, SpecificationEntity.Type t, String key)
String getRespects(String domain, SpecificationEntity.Type t)
String getRespects(Set<Map.Entry<String,SpecificationEntity.Type>> oneRespect, SpecificationEntity.Type t)
String getSpecification()
private void put(String key, Map.Entry<String,SpecificationEntity.Type> value)
private void put(String key, SpecificationEntity.Type t, String value)