Uses of Package
dev.civl.mc.semantics.IF

Packages that use dev.civl.mc.semantics.IF

Package	Description
dev.civl.mc.kripke.IF	Module kripke provides the definition of various transitions and the enabler and state manager of CIVL.
dev.civl.mc.predicate.IF	Module predicate defines predicates that are required to hold for any CIVL-C programs.
dev.civl.mc.semantics.IF	Module semantics implements the semantics of CIVL-C.
dev.civl.mc.util.IF	Module util provides various general-purpose utilities used by CIVL.

Classes in dev.civl.mc.semantics.IF used by dev.civl.mc.kripke.IF

Class	Description
Evaluator	This is the CIVL main evaluator.
Executor
LibraryEvaluatorLoader	The library evaluator loader provides the mechanism for loading the library evaluator of a certain library.
LibraryLoaderException	A library loader exception is produced by errors occur during when a library executor/evaluator/enabler loader attempts to load a specific library executor/evaluator/enabler.
SymbolicAnalyzer	This class provides methods dealing with symbolic expressions and states, which represent some common-used operations like obtaining a sub-array from a given array, etc.
Transition	This represents a CIVL transition, which is deterministic and enabled at a certain state.

Classes in dev.civl.mc.semantics.IF used by dev.civl.mc.predicate.IF

Class	Description
Evaluator	This is the CIVL main evaluator.
SymbolicAnalyzer	This class provides methods dealing with symbolic expressions and states, which represent some common-used operations like obtaining a sub-array from a given array, etc.

Classes in dev.civl.mc.semantics.IF used by dev.civl.mc.semantics.IF

Class	Description
ArrayToolBox	This interface provides a collection of methods that manipulating symbolic expressions whose symbolic type has ARRAY kind.
ArrayToolBox.ArrayShape	The data structure for describing array shapes, including dimensions, extent for each dimension and slice size for each sub-array with lower dimension.
ArrayToolBox.ArraySlice	the data structure for describing array slices.
Evaluation	Represents the result of evaluating an expression in two parts: the (possibly) new state resulting from side-effects arising from the evaluation, and the value resulting from the evaluation.
Evaluator	This is the CIVL main evaluator.
Executor
Format
Format.ConversionType
LibraryEvaluator	A Library Evaluator provides a method to "evaluate" the guard of each system function call.
LibraryEvaluatorLoader	The library evaluator loader provides the mechanism for loading the library evaluator of a certain library.
LibraryExecutor	A Library Executor provides the semantics for system functions defined in a library.
LibraryExecutorLoader	The library executor loader provides the mechanism for loading the library executor of a certain library.
LibraryLoaderException	A library loader exception is produced by errors occur during when a library executor/evaluator/enabler loader attempts to load a specific library executor/evaluator/enabler.
MemoryUnitExpressionEvaluator
SymbolicAnalyzer	This class provides methods dealing with symbolic expressions and states, which represent some common-used operations like obtaining a sub-array from a given array, etc.
Transition	This represents a CIVL transition, which is deterministic and enabled at a certain state.
Transition.TransitionKind
TypeEvaluation	Represents the result of evaluating something that returns a symbolic type, but in two parts: the (possibly) new state resulting from side-effects arising from the evaluation, and the symbolic type resulting from the evaluation.

Classes in dev.civl.mc.semantics.IF used by dev.civl.mc.util.IF

Class	Description
Evaluator	This is the CIVL main evaluator.