wp.md

layout: plugin
title: WP
description: Deductive proofs of ACSL contracts.
key: main
distrib_mode: main
manual_pdf: /download/frama-c-wp-manual.pdf
additional:
  - name:  "ACSL by Example, by Fraunhofer FOKUS"
    short: "ACSL by Example"
    link:  https://fraunhoferfokus.github.io/acsl-by-example
  - name:  "Introduction to C program proof with Frama-C and WP, by Allan Blanchard"
    short: "Tutorial on Frama-C and WP"
    link:  https://github.com/AllanBlanchard/tutoriel_wp

Overview

This plug-in allows proving that ACSL contracts are fulfilled for all possible executions of the code. It is based on weakest-precondition calculus and relies on external automated provers and proof assistants to finalize the assessment of the desired properties.

Proving properties by WP is a modular approach, which makes it a strong alternative to consider in replacement of traditional unit testing.

Quick Start

frama-c -wp file.c

Technical Notes

• Maturity: industrialized.
• WP has an internal prover, Qed, which is also used to simplify proof obligations before they are sent to external provers.

Recommended External Provers:

• Alt-Ergo
• Coq
• Z3
• CVC4

And all other provers supported by the Why3 platform.

Further Reading

For more details about the WP plug-in, including installation instructions, please consult the WP manual.

Besides the manual, the WP plug-in is used in some tutorials:

• {{page.additional[0].name}};

This tutorial, written by the Fraunhofer FOKUS team, provides an extensive corpus of ACSL annotations for typical C programs to be proved by WP. It is available online and a public repository hosts the annotated source examples.

• {{page.additional[1].name}};

This tutorial, written by Allan Blanchard, introduces several notions of program proof before describing ACSL and WP, and how to perform proofs using Frama-C.

Dependencies

This plug-in can (optionally) use the results of the RTE plug-in.