Frama-C (FRAmework for Modular Analysis of C programs) is a set of interoperable program analyzers for C programs. I have used this software during all my PhD thesis and after, mostly for deductive proof using the WP plugin. So, I wrote a tutorial that allows to learn ACSL (the specification language of Frama-C) and the use of WP by practice, also getting some theorical rudiments about deductive proof.
It can be used for both learning and teaching, I hope you will have some fun with it :) .
The last version is available on my website in English and in French.
An online French version is available on Zeste de Savoir.
In order to build the files, you can use docker
docker build -t tutoriel_wp .
docker run --rm -v $PWD:/mnt -w /mnt tutoriel_wp make