Visual DbC is a proof management and visualization tool. It allows to visualize code members (e.g. types, attributes, methods) together with specifications (e.g. method contracts, invariants) and proofs in a DbC diagram similar to an UML class diagram. Proof references are used to indicate that a code member or a specification is used by a proof.
The following sections illustrate the main features of Visual DbC using screenshots.
Each section contains numbered screenshots that explain a usage scenario step by step.
Clicking on each picture produces a more detailed view.
The screenshots may differ from the latest release.
Visual DbC is compatible with Eclipse Indigo (3.7) or newer.
Required update-sites and installation instructions are available in the download area.
Visualize existing source code
Do proofs with a DbC diagram
Visualize proof dependencies of a proof in the KeYIDE