| Package | Description |
|---|---|
| edu.udel.cis.vsl.tass |
Root of the TASS source tree.
|
| edu.udel.cis.vsl.tass.ast | |
| edu.udel.cis.vsl.tass.ast.IF | |
| edu.udel.cis.vsl.tass.ast.IF.declaration | |
| edu.udel.cis.vsl.tass.ast.IF.expression | |
| edu.udel.cis.vsl.tass.ast.IF.statement | |
| edu.udel.cis.vsl.tass.ast.IF.type | |
| edu.udel.cis.vsl.tass.ast.impl | |
| edu.udel.cis.vsl.tass.ast.impl.declaration | |
| edu.udel.cis.vsl.tass.ast.impl.expression | |
| edu.udel.cis.vsl.tass.ast.impl.pragmaParser | |
| edu.udel.cis.vsl.tass.ast.impl.statement | |
| edu.udel.cis.vsl.tass.ast.impl.type | |
| edu.udel.cis.vsl.tass.ast.parser | |
| edu.udel.cis.vsl.tass.ast2model.IF | |
| edu.udel.cis.vsl.tass.ast2model.impl | |
| edu.udel.cis.vsl.tass.config |
Provides configuration classes used during verification.
|
| edu.udel.cis.vsl.tass.dynamic |
Provides the functionalities to create and manipulate different
kinds of values during TASS verification process.
|
| edu.udel.cis.vsl.tass.dynamic.IF |
Interface package for the dyanmic module: deals with all runtime objects
that occur in execution a TASS model.
|
| edu.udel.cis.vsl.tass.dynamic.IF.cell |
Interface package for module dynamic.cell: a cell is a runtime variable.
|
| edu.udel.cis.vsl.tass.dynamic.IF.simplify |
Interface package for module dynamic.simplify: provides functionality
for simplifying dynamic objects, such as values, dynamic types, messages,
and so on.
|
| edu.udel.cis.vsl.tass.dynamic.IF.type |
Interface package for module dynamic.type: provides representations of runtime
types.
|
| edu.udel.cis.vsl.tass.dynamic.IF.value |
Interface package for module dynamic.value: provides representations
of runtime values that occur in the execution of a TASS model.
|
| edu.udel.cis.vsl.tass.dynamic.impl |
Implementation package for the dyanmic module: deals with all runtime objects
that occur in execution a TASS model.
|
| edu.udel.cis.vsl.tass.dynamic.impl.cell |
Implementation package for module dynamic.cell: a cell is a runtime variable.
|
| edu.udel.cis.vsl.tass.dynamic.impl.simplify |
Implementation package for module dynamic.simplify: provides functionality
for simplifying dynamic objects, such as values, dynamic types, messages,
and so on.
|
| edu.udel.cis.vsl.tass.dynamic.impl.type |
Implementation package for module dynamic.type: provides representations of runtime
types.
|
| edu.udel.cis.vsl.tass.dynamic.impl.value |
Implementation package for module dynamic.value: provides representations
of runtime values that occur in the execution of a TASS model.
|
| edu.udel.cis.vsl.tass.front |
The front-end module for TASS: provided functionality for transforming source
codes in various languages into a TASS model.
|
| edu.udel.cis.vsl.tass.front.minimp |
The front-end module based on the Antlr-generated parser for a subset of C.
|
| edu.udel.cis.vsl.tass.front.minimp.ast.declaration |
The declaration submodule of the AST module.
|
| edu.udel.cis.vsl.tass.front.minimp.ast.expression |
The expression submodule of the AST module.
|
| edu.udel.cis.vsl.tass.front.minimp.ast.misc |
A package for miscellaneous classes withing the AST module.
|
| edu.udel.cis.vsl.tass.front.minimp.ast.statement |
The statement submodule of the AST module.
|
| edu.udel.cis.vsl.tass.front.minimp.ast.type |
The type submodule of the AST module.
|
| edu.udel.cis.vsl.tass.front.minimp.lib |
The library submodule of module front.minimp deals with program libraries.
|
| edu.udel.cis.vsl.tass.front.minimp.parser |
The minimp.parser package contains the MiniMP grammar and the Antlr-generated lexer and parser classes.
|
| edu.udel.cis.vsl.tass.gui.IF |
The interface for the GUI module.
|
| edu.udel.cis.vsl.tass.gui.impl |
The implementation of the GUI module.
|
| edu.udel.cis.vsl.tass.kripke |
Kripke module: provides classes that define the state-transition system of
a TASS system.
|
| edu.udel.cis.vsl.tass.kripke.IF |
Interface for the Kripke module: provides classes that define the state-transition system of
a TASS system.
|
| edu.udel.cis.vsl.tass.kripke.impl |
Implementation for the Kripke module: provides classes that define the state-transition system of
a TASS system.
|
| edu.udel.cis.vsl.tass.library | |
| edu.udel.cis.vsl.tass.library.impl | |
| edu.udel.cis.vsl.tass.library.libfoo | |
| edu.udel.cis.vsl.tass.library.libmpi | |
| edu.udel.cis.vsl.tass.library.libmpp |
The "MiniMP Message Passing" (MPP) library module.
|
| edu.udel.cis.vsl.tass.library.libstdio | |
| edu.udel.cis.vsl.tass.library.libstdlib | |
| edu.udel.cis.vsl.tass.log |
The log module: logs are created during a TASS verification run to record
property violations discovered.
|
| edu.udel.cis.vsl.tass.log.IF |
Public interface for the log module: logs are created during a TASS verification run to record
property violations discovered.
|
| edu.udel.cis.vsl.tass.log.impl |
Implementation of the log module: logs are created during a TASS verification run to record
property violations discovered.
|
| edu.udel.cis.vsl.tass.model |
The model module: provides classes to represent, construct, and manipulate
the primary intermediate representation in TASS: the TASS modle.
|
| edu.udel.cis.vsl.tass.model.IF |
The public interface of the model module: provides interfaces to represent,
construct, and manipulate the primary intermediate representation in TASS:
the TASS model.
|
| edu.udel.cis.vsl.tass.model.IF.expression |
The public interface for submodule model.expression, used to manipulate
expressions in a TASS model.
|
| edu.udel.cis.vsl.tass.model.IF.location |
The public interface of the model.location submodule: provides interfaces
to represent the different kinds of locations that can occur in the
TASS representation of a function (procedure).
|
| edu.udel.cis.vsl.tass.model.IF.scope | |
| edu.udel.cis.vsl.tass.model.IF.statement |
The public interface of the model.statement submodule: provides interfaces
to represent the different kinds of statements that can occur in the
TASS representation of a function (procedure).
|
| edu.udel.cis.vsl.tass.model.IF.type |
The public interface of the model.type submodule: provides interfaces
to represent the different kinds of (static) types that can occur in
TASS models.
|
| edu.udel.cis.vsl.tass.model.IF.variable |
The public interface of the model.variable submodule: provides interfaces
to represent the different kinds of (static) variables that can occur in
TASS expressions and models.
|
| edu.udel.cis.vsl.tass.model.impl |
The implementation of the model module.
|
| edu.udel.cis.vsl.tass.model.impl.expression |
Implementation package for module model.expression.
|
| edu.udel.cis.vsl.tass.model.impl.expression.literal |
Implementation of literal expressions.
|
| edu.udel.cis.vsl.tass.model.impl.lib |
Experimental package for implementating library functionality.
|
| edu.udel.cis.vsl.tass.model.impl.location |
Implementation package for module model.location.
|
| edu.udel.cis.vsl.tass.model.impl.scope | |
| edu.udel.cis.vsl.tass.model.impl.statement |
Implementation package for module model.statement.
|
| edu.udel.cis.vsl.tass.model.impl.type |
Implementation package for module type.
|
| edu.udel.cis.vsl.tass.model.impl.variable |
Implementation package for module model.variable.
|
| edu.udel.cis.vsl.tass.morph |
The morph module: provides classes supporting the Morphic Pattern,
as described in Section 5 of Siegel and Zirkel, The Toolkit for
Accurate Scientific Software, Technical Report UD-CIS-2011-01,
University of Delaware, 2011.
|
| edu.udel.cis.vsl.tass.number |
A utility package supporting infinite precision integer and rational numbers,
and a variety of arithmetic operations on them.
|
| edu.udel.cis.vsl.tass.number.IF |
The interface package for the
number module. |
| edu.udel.cis.vsl.tass.number.real |
An implementation of the
number module. |
| edu.udel.cis.vsl.tass.predicate |
The TASS
predicate module deals wtih predicates on the global states
of a TASS state-transition system. |
| edu.udel.cis.vsl.tass.predicate.IF |
The interface to the TASS
predicate module. |
| edu.udel.cis.vsl.tass.predicate.impl |
An implementation of the
predicate module. |
| edu.udel.cis.vsl.tass.prove |
Provides classes to solve the queries from backend during
verification process.
|
| edu.udel.cis.vsl.tass.prove.cvc | |
| edu.udel.cis.vsl.tass.prove.ideal | |
| edu.udel.cis.vsl.tass.prove.IF | |
| edu.udel.cis.vsl.tass.search |
Provide generic depth first search service to TASS back-end during
verification process.
|
| edu.udel.cis.vsl.tass.semantics |
Provide classes to process the semantic information in the components of
a TASS model.
|
| edu.udel.cis.vsl.tass.semantics.IF | |
| edu.udel.cis.vsl.tass.semantics.impl | |
| edu.udel.cis.vsl.tass.simplify |
Provide classes to simplify symbolic expressions.
|
| edu.udel.cis.vsl.tass.simplify.IF | |
| edu.udel.cis.vsl.tass.simplify.light | |
| edu.udel.cis.vsl.tass.state |
Provide classes to create new states for TASS verification process.
|
| edu.udel.cis.vsl.tass.state.IF | |
| edu.udel.cis.vsl.tass.state.impl | |
| edu.udel.cis.vsl.tass.symbolic |
Provide classes to create and manipulate different kinds of symbolic
expressions.
|
| edu.udel.cis.vsl.tass.symbolic.affine | |
| edu.udel.cis.vsl.tass.symbolic.array | |
| edu.udel.cis.vsl.tass.symbolic.cast | |
| edu.udel.cis.vsl.tass.symbolic.cnf | |
| edu.udel.cis.vsl.tass.symbolic.concrete | |
| edu.udel.cis.vsl.tass.symbolic.cond | |
| edu.udel.cis.vsl.tass.symbolic.constant | |
| edu.udel.cis.vsl.tass.symbolic.expression | |
| edu.udel.cis.vsl.tass.symbolic.factor | |
| edu.udel.cis.vsl.tass.symbolic.factorpoly | |
| edu.udel.cis.vsl.tass.symbolic.function | |
| edu.udel.cis.vsl.tass.symbolic.ideal | |
| edu.udel.cis.vsl.tass.symbolic.ideal.simplify | |
| edu.udel.cis.vsl.tass.symbolic.IF | |
| edu.udel.cis.vsl.tass.symbolic.IF.tree | |
| edu.udel.cis.vsl.tass.symbolic.IF.type | |
| edu.udel.cis.vsl.tass.symbolic.integer | |
| edu.udel.cis.vsl.tass.symbolic.monic | |
| edu.udel.cis.vsl.tass.symbolic.monomial | |
| edu.udel.cis.vsl.tass.symbolic.polynomial | |
| edu.udel.cis.vsl.tass.symbolic.power | |
| edu.udel.cis.vsl.tass.symbolic.rational | |
| edu.udel.cis.vsl.tass.symbolic.relation | |
| edu.udel.cis.vsl.tass.symbolic.standard | |
| edu.udel.cis.vsl.tass.symbolic.tuple | |
| edu.udel.cis.vsl.tass.symbolic.type | |
| edu.udel.cis.vsl.tass.symbolic.util | |
| edu.udel.cis.vsl.tass.trace | |
| edu.udel.cis.vsl.tass.transition | |
| edu.udel.cis.vsl.tass.transition.IF | |
| edu.udel.cis.vsl.tass.transition.impl | |
| edu.udel.cis.vsl.tass.ui | |
| edu.udel.cis.vsl.tass.util |
Provide different utility classes to TASS components.
|
| edu.udel.cis.vsl.tass.verify |
Provide classes to verify a TASS model or compare two models.
|
| edu.udel.cis.vsl.tass.verify.impl |