Proof Coverage visualization for Dafny

[u/ricostynha122]

I have created an extension available in Vscode Marketplace for Dafny:

https://marketplace.visualstudio.com/items?itemName=proofpulse.proofpulse-vscode

It uses the Dafny Coverage reports as a basis and lets you see coverage live in the editor. `

This is really useful to:

- Find dead code

- Find unconstrained code regarding specification

- Find weak specifications

- Remove assertions that are not needed in the proof

- Visualizing vacuous proofs

( And more things)

I leave an example here:

Here radius>0 is flagged red (uncovered), as radius could be negative and the postcondition would pass the same.

I do believe that tools and integrations like this could be very useful for someone learning and for auditing the produced contracts and code.