ETH Logo

CITADEL

What is CITADEL

CITADEL (Contract Inference Tool that Applies Daikon to the Eiffel Language) is an Eiffel front-end for the Daikon assertion detector. With CITADEL you can strengthen and correct contracts in your Eiffel classes. All you need to do is to give CITADEL a system that exercises these classes!

A dynamic assertion detector is a tool that determines conditions holding throughout a software system execution. After these conditions have been found developers can assume that they also hold for all other executions and therefore form a specification (a set of contracts) of the system.

Dynamic contract inference system consists of several components, as shown in the figure below.

Dynamic contract inference system

The main steps involved in the contract inference process are the following:

  1. An instrumenter modifies the program source so that, at certain program points, it saves the values of the variables in scope to a data trace file. The instrumenter also produces program point declarations (static information about program points and variables).
  2. The instrumented program is exercised through a test suite. Each run of the program results in a data trace file.
  3. Daikon instantiates assertion templates from its list using variables of appropriate types. This results in a list of potential assertions, which are then checked against the variable values recorded in the data trace files.
  4. The inferred assertions can be post-processed, for instance by a pretty-printer, and inserted into the original source code as annotations.

Out of these components, only the instrumenter and the postprocessor depend on the programming language in which the original system is written. These two components form a front-end that allows the universal assertion detector to work for software systems written in different languages (and even with data that was generated through other means than during program execution). CITADEL is one of such front-ends that allows Daikon to work with software systems written in Eiffel.

For further details please refer to the CITADEL documentation

Downloads