Package jml2b.pog.substitution

Provides the classes necessary to create and manage substitutions.

See:
Description

Interface Summary

Substitution

This interface describes a substitution.

Class Summary

SubArrayElement	This class corresponds to the substitution of xxxelements with a formula.
SubArrayElementSingle	This class corresponds to the substitution of xxxelements with a xxxelements <+ {f |-> xxxelements(f) <+ {i |-> v}}.
SubArrayLength	This class corresponds to the substitution of arraylength with a formula.
SubForm	This class corresponds to the substitution of a formula by another.
SubInstances	This class corresponds to the substitution of instances with: instances \/ f instances \/ {f}
SubInstancesSet	This class corresponds to the substituion of instances with instances \/ f.
SubInstancesSingle	This class corresponds to the substituion of instances with instances \/ {f} corresponding to an instance creation.
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.
SubStaticOrLocalField
SubTmpVar	This class corresponds to the substitution of a tempory variable with a formula.
SubTypeof	This abstract class describes substitutions applied on typeof
SubTypeofSet	This interface describes a substitution of typeof by typeof <+ f * {t}
SubTypeofSingle	This interface describes a substitution of typeof by typeof <+ {f |-> t}

Package jml2b.pog.substitution Description

Provides the classes necessary to create and manage substitutions.

Substitutions applied to goal are stored in manner to display the goal in the Java view in the most closest way to Java possible. That means that rather diplaying the goal where substitution have been applied, the goal is displayed as its original formula (coming directly from the Java source) and subtitutions are displayed below describing the runtime behaviour that has been applied on the goal.

This package defines an interface and its implementing classes that correspond to each type of substitution that can be done during the WP calculus.

Package Specification

Related Documentation