| java.lang.Object
 U2.T2.Trace
| Trace | | public class Trace implements Serializable(Code) | | This class provides a meta representation of execution. An instance
of this class is called an execution trace. It is a meta
representation of an actual execution. For the big picture, see the
doc of the
U2.T2 U2.T2 package . The important thing is that
from an execution trace we can reproduce the actual execution. It
can also be saved and reloaded; thus allowing us to later on replay
the actual execution.
A trace consists of a creation step, that creates the
target object, and a sequence of subsequent
U2.T2.Trace.TraceStep trace steps , each doing something on the
target object, e.g. calling a method on it. The creation step is an
instance of so called a
U2.T2.Trace.MkValStep MkVal step. A
MkVal step is used to create an object, whereas a trace step is
used to apply side effect on the target object. A trace step may
also consist of MkVal steps, e.g. when it needs to create objects
to pass as parameters to a method.
|
| Inner Class :abstract public static class MkValStep implements Serializable | |
| Inner Class :public static class REF extends MkValStep | |
| Inner Class :public static class CONST extends MkValStep | |
| Inner Class :public static class CREATE_TARGET_OBJECT extends MkValStep | |
| Inner Class :public static class CREATE_COLLECTION_LIKE extends MkValStep | |
| Inner Class :abstract public static class TraceStep implements Serializable | |
| Inner Class :public static class UPDATE_FIELD extends TraceStep | |
| Inner Class :public static class CALL_METHOD extends TraceStep | |
| Inner Class :public static class ExecResult | |
| Constructor Summary | |
| public | Trace()
Create an empty execution trace. |
| Method Summary | |
| public static ExecResult | MkTargetObject(Pool pool, MkValStep step, Method classinv)
As MkVal, but especially for constructing a target object. | | public static Object | MkVal(Pool pool, MkValStep step)
Execute a given MkVal step to construct an object. | | public static Object[] | MkVal(Pool pool, MkValStep[] steps)
As the other MkVal, but this one executes multiple steps. | | public static ExecResult | exec(Pool pool, Object targetObj, TraceStep step, Method classinv, PrintStream out, boolean printMethodParamsOption, Show Shower)
Execute a given trace step. | | public static ExecResult | exec(Pool pool, Object targetObj, TraceStep step, Method classinv)
As the other exec, but this does not produce report. | | public static void | execClassInv(Method classinv, Object targetObj, ExecResult result)
Execute (and check) the given class invariant.
Parameters:
classinv - The method specifying the class invariant.
Parameters:
result - Information about violations found will be put in here. | | public static LinkedList<Trace> | load(Class CUT)
For loading execution traces from a single save-file. | | public static void | main(String[] args)
| | public void | report(Pool pool, Method classinv, PrintStream out)
This method is used to report the states, methods called,
parameters passed along an execution induced by a trace. | | public static void | save(Class CUT, LinkedList<Trace> traces)
For saving execution traces. | | protected static void | update_aux_laststep(Object targetObj, String step)
Method to fill-in the aux_laststep hook. |
| VIOLATING_TRACE | | public static String VIOLATING_TRACE(Code) | | Currently this is the only classification :)
|
| classification | | String classification(Code) | | Used to classify different kind of traces, e.g. to distinguish
violating and non-violating traces. The purpose of this field is
mainly to quickly filter traces without having to execute them.
|
| creation | | MkValStep creation(Code) | | The creation step that starts this execution trace.
|
| indexOfTargetObj | | int indexOfTargetObj(Code) | | The target object of this execution trace.
|
| printIntermediateStepsOption | | boolean printIntermediateStepsOption(Code) | | |
| printMethodParamsOption | | boolean printMethodParamsOption(Code) | | |
| trace | | LinkedList<TraceStep> trace(Code) | | The sequence of trace steps belonging to this execution trace.
|
| Trace | | public Trace()(Code) | | Create an empty execution trace.
|
| MkTargetObject | | public static ExecResult MkTargetObject(Pool pool, MkValStep step, Method classinv) throws InvocationTargetException(Code) | | As MkVal, but especially for constructing a target object. It will
also execute the classinvariant.
|
| exec | | public static ExecResult exec(Pool pool, Object targetObj, TraceStep step, Method classinv, PrintStream out, boolean printMethodParamsOption, Show Shower)(Code) | | Execute a given trace step. If a printstream is also given, this
methdo will also report the execution to the stream.
Parameters:
out - If not null will cause objects involed in this step to be textually reported to this print stream.
Parameters:
printMethodParamsOption - If true, and if this step is a methodcalls, the parameters to the call will be printedin the report.
Parameters:
Shower - A shower object need to be passed; it is used toshow (print) an object, but we also need to maintain objectnumbering across different the entire execution; the showobject internally maintains this numbering. |
| exec | | public static ExecResult exec(Pool pool, Object targetObj, TraceStep step, Method classinv)(Code) | | As the other exec, but this does not produce report.
|
| execClassInv | | public static void execClassInv(Method classinv, Object targetObj, ExecResult result)(Code) | | Execute (and check) the given class invariant.
Parameters:
classinv - The method specifying the class invariant.
Parameters:
result - Information about violations found will be put in here. |
| load | | public static LinkedList<Trace> load(Class CUT) throws T2Exception(Code) | | For loading execution traces from a single save-file. The file
is assumed to be called name.tr where name is CUT's simple name.
Parameters:
CUT - The target class to which the traces belong. |
| report | | public void report(Pool pool, Method classinv, PrintStream out)(Code) | | This method is used to report the states, methods called,
parameters passed along an execution induced by a trace. Note
that to be able to do so, the execution has to be
reconstructed. Violations will not be checked. This is assumed
to has been done by whatever phases that preceed reporting.
Parameters:
pool - Pass here the same pool as used to produce thisexecution trace.
Parameters:
out - The steam to which the report will be printed;should not be null. |
| save | | public static void save(Class CUT, LinkedList<Trace> traces) throws T2Exception(Code) | | For saving execution traces. They will be saved in the file
name.tr where name is CUT's simple name.
Parameters:
CUT - The target class to which the traces belong. |
| update_aux_laststep | | protected static void update_aux_laststep(Object targetObj, String step)(Code) | | Method to fill-in the aux_laststep hook.
|
|
|