Package de.uka.ilkd.key.util.rifl

RIFL is short for "Requirements for Information Flow Language", a tool-indepentent specification language developed in the RS3 project.

See: Description

Interface Summary

Interface	Description
SpecificationContainer	Container for parsed RIFL specifications.

Class Summary

Class	Description
DefaultSpecificationContainer	Default implementation of SpecificationContainer.
RIFLHandler	XML content handler for the RIFL language.
RIFLHandler.ErrorHandler
RIFLTransformer	Facet class for interpreting RIFL specifications.
SecurityLattice	A lattice of security domains in RIFL.
SimpleRIFLExceptionHandler	Simple exception handler which just writes to standard output.
SpecificationEntity	Program elements which may be named as sources or sinks in RIFL/Java.
SpecificationEntity.Field
SpecificationEntity.Parameter
SpecificationEntity.ReturnValue
SpecificationInjector	Writes JML* translation of RIFL specifications to Java files.
SpecificationInjector.JMLFactory	Produces JML* respects clauses.

Enum Summary

Enum	Description
SpecificationEntity.Type

Package de.uka.ilkd.key.util.rifl Description

RIFL is short for "Requirements for Information Flow Language", a tool-indepentent specification language developed in the RS3 project. The RIFL/Java dialect is documented in XXX. This package contains a transformer from input RIFL files (XML) and original Java files to JML* annotated files.