Commits on Aug 14, 2023

1. Feat: Added the test command …

   Fixes #417
   This PR adds the "Test" command in the contextual Dafny menu.
   
   A bit of context. It's not possible to put several Main methods in included files, but it's definitely possible to put tests in each file as needed.
   Currently, to run tests, one typically right-clicks "Dafny > build with custom arguments", and then replace everything with "test". There is not even a shortcut for that, although the "test" command is fully supported in Dafny.
   Moreover, I am adding the "--no-verify" flag by default both on tests and run because
   1) it's in the context of a development environment
   2) The minimum required for `dafny run` and `dafnyt test` is that the program resolves and the compiler can compile it.
   3) Verification of the entire file before testing is at best redundant because it was already verified in the IDE, at worst it forces the user to add a bunch of "assume false" in their code just because they haven't prove some assertions they conjectured.
   
   I think it's fair to say that the usual workflow of testing is complementary to verification, meaning it makes it possible to experiment on specifications before proving them.

   

   MikaelMayer committed Aug 14, 2023
   Configuration menu

   • View commit details
   • Copy full SHA for 0738dc8
   • Browse repository at this point

   Copy the full SHA

   0738dc8 View commit details

   Browse the repository at this point in the history

2. Fixed warnings and errors

   

   MikaelMayer committed Aug 14, 2023
   Configuration menu

   • View commit details
   • Copy full SHA for 9e483dd
   • Browse repository at this point

   Copy the full SHA

   9e483dd View commit details

   Browse the repository at this point in the history