wp.md 2.16 KB
Newer Older
1
2
3
4
5
6
---
layout: plugin
title: WP
description: Deductive proofs of ACSL contracts.
key: main
distrib_mode: main
7
priority: 0
8
manual_pdf: /download/frama-c-wp-manual.pdf
9
additional:
Allan Blanchard's avatar
Allan Blanchard committed
10
11
  - name:  "ACSL by Example, by Fraunhofer FOKUS"
    short: "ACSL by Example"
Allan Blanchard's avatar
Allan Blanchard committed
12
    link:  https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf
Allan Blanchard's avatar
Allan Blanchard committed
13
  - name:  "Introduction to C program proof with Frama-C and WP, by Allan Blanchard"
14
    short: "Tutorial on Frama-C/WP"
Allan Blanchard's avatar
Allan Blanchard committed
15
    link:  https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
---

## 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.

40
Recommended External Provers:
41
42
43
44
45
46
47
48
49
50
51
52
53
54
- Alt-Ergo
- Coq
- Z3
- CVC4

And all other provers supported by the [Why3](http://why3.lri.fr) platform.

## Further Reading

For more details about the **WP** plug-in, including installation instructions,
please consult the [WP manual]({{page.manual_pdf}}).

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

55
- [{{page.additional[0].name}}]({{page.additional[0].link}});
56
57
58
59
60
61

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

62
- [{{page.additional[1].name}}]({{page.additional[1].link}});
63
64
65
66
67
68
69
70

This tutorial, written by Allan Blanchard, introduces several notions of program
proof before describing [ACSL](/html/acsl.html) and **WP**, and how to perform
proofs using Frama-C.

## Dependencies

This plug-in can (optionally) use the results of the [RTE](rte.html) plug-in.