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.