dafny-lang / dafny-reportgenerator

A tool for analyzing and reporting on Dafny, especially the results of verification
MIT License
3 stars 4 forks source link

Add coefficient of variance (CV) limit option #11

Closed atomb closed 2 years ago

atomb commented 2 years ago

This PR adds support for normalized standard deviation (also known as coefficient of variance, or CV) analysis. This is a more standardized and likely user-friendly way to look at how much values vary. Settling on a standard limit of, say, 20% might be reasonable (or maybe less?).

This PR adds the new analysis to CI (with a limit of 5%). It also includes some refactoring to improve stability of its own code. It also fixes a bug in double to BigRational (real) conversion.

robin-aws commented 2 years ago

(with a limit of 65% because some of the libraries code isn't very stable)

Let's investigate why this project is re-verifying the libraries submodule code, it shouldn't be.

robin-aws commented 2 years ago

(with a limit of 65% because some of the libraries code isn't very stable)

Let's investigate why this project is re-verifying the libraries submodule code, it shouldn't be.

In fact it looks to me like it isn't: https://github.com/dafny-lang/dafny-reportgenerator/runs/7012967474?check_suite_focus=true

atomb commented 2 years ago

(with a limit of 65% because some of the libraries code isn't very stable)

Let's investigate why this project is re-verifying the libraries submodule code, it shouldn't be.

In fact it looks to me like it isn't: https://github.com/dafny-lang/dafny-reportgenerator/runs/7012967474?check_suite_focus=true

Oh, you're right! It's code in the StandardLibrary module in this repository. :) So we could fix that with a commit to this repo. So I'll add some further stability refactoring to get those numbers down.

atomb commented 2 years ago

It turns out that more stability refactoring isn't needed, after merging with the other PRs (which include updating to the latest Dafny). I'm very happy with the bounds in CI now! :)