Uses of Interface
jml2b.pog.substitution.Substitution

Packages that use Substitution

jml2b.pog.lemma
jml2b.pog.substitution	Provides the classes necessary to create and manage substitutions.

Uses of Substitution in jml2b.pog.lemma

Methods in jml2b.pog.lemma with parameters of type Substitution

void	ExsuresLemma.sub(Substitution s)
void	Goal.sub(Substitution s)
void	ILemma.sub(Substitution s) Apply a substitution to the lemma.
Proofs	Proofs.sub(Substitution s) Apply a substitution to the content of the proof.
void	SimpleLemma.sub(Substitution s)
void	TheoremList.sub(Substitution s) Apply a substitution to the theorem list.

Uses of Substitution in jml2b.pog.substitution

Classes in jml2b.pog.substitution that implement Substitution

class	SubArrayElement This class corresponds to the substitution of xxxelements with a formula.
class	SubArrayElementSingle This class corresponds to the substitution of xxxelements with a xxxelements <+ {f |-> xxxelements(f) <+ {i |-> v}}.
class	SubArrayLength This class corresponds to the substitution of arraylength with a formula.
class	SubForm This class corresponds to the substitution of a formula by another.
class	SubInstances This class corresponds to the substitution of instances with: instances \/ f instances \/ {f}
class	SubInstancesSet This class corresponds to the substituion of instances with instances \/ f.
class	SubInstancesSingle This class corresponds to the substituion of instances with instances \/ {f} corresponding to an instance creation.
class	SubMemberField This class implements a substitution of a member field a by a <+ { b |-> c } corresponding to an affectation of a new value for a given instance.
class	SubStaticOrLocalField
class	SubTmpVar This class corresponds to the substitution of a tempory variable with a formula.
class	SubTypeof This abstract class describes substitutions applied on typeof
class	SubTypeofSet This interface describes a substitution of typeof by typeof <+ f * {t}
class	SubTypeofSingle This interface describes a substitution of typeof by typeof <+ {f |-> t}

Methods in jml2b.pog.substitution with parameters of type Substitution

void	SubArrayElement.sub(Substitution s)
void	SubArrayElementSingle.sub(Substitution s)
void	SubArrayLength.sub(Substitution s)
void	SubForm.sub(Substitution s)
void	SubInstances.sub(Substitution s)
void	SubMemberField.sub(Substitution s)
void	SubTmpVar.sub(Substitution s)
void	SubTypeof.sub(Substitution s)
void	Substitution.sub(Substitution s) Apply a substitution on the current substitution.