|
|||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object jml2b.util.Profiler jml2b.pog.substitution.SubTypeof jml2b.pog.substitution.SubTypeofSingle
This interface describes a substitution of typeof
by
typeof <+ {f |-> t}
Field Summary |
Fields inherited from interface jml2b.pog.substitution.Substitution |
ARRAY_ELEMENT, ARRAY_ELEMENT_SINGLE, ARRAY_LENGTH, FORM, INSTANCES_SET, INSTANCES_SINGLE, MEMBER_FIELD, TMP_VAR, TYPEOF_SET, TYPEOF_SINGLE |
Constructor Summary | |
SubTypeofSingle(Formula f,
Formula t)
Constructs a substitution for typeof |
Method Summary | |
java.lang.Object |
clone()
Clones the substitution. |
void |
save(IJml2bConfiguration config,
JpoOutputStream s,
IJmlFile jf)
Saves the substitution in a .jpo file |
Formula |
sub(Formula p)
Substitues typeof by typeof <+ {f |-> t} in
p . |
Methods inherited from class jml2b.pog.substitution.SubTypeof |
getF, getT, sub |
Methods inherited from class jml2b.util.Profiler |
runGC |
Methods inherited from class java.lang.Object |
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Constructor Detail |
public SubTypeofSingle(Formula f, Formula t)
typeof
f
- The formula corresponding to the extended typeof domaint
- The formula corresponding to the value asociated to new domainMethod Detail |
public java.lang.Object clone()
Substitution
clone
in interface Substitution
clone
in class SubTypeof
public Formula sub(Formula p)
typeof
by typeof <+ {f |-> t}
in
p
.
p
- The formula on which the substitution is applied
public void save(IJml2bConfiguration config, JpoOutputStream s, IJmlFile jf) throws java.io.IOException
Substitution
save
in interface Substitution
save
in class SubTypeof
java.io.IOException
|
|||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |