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