Comment annotations

[nono]

Hello,

esverify looks nice. I think it may be more practical for existing projects to put the ensures and requires annotations in comments, to avoid any side-effect during the execution. You may be inspired by the comment types of Flow: https://flow.org/en/docs/types/comments/.

The example in the README could look like this:

function max(a, b) {
  /*-@
  requires(typeof a === "number");
  requires(typeof b === "number");
  ensures(res => res >= a);
  */

  if (a >= b) {
    return a;
  } else {
    return b;
  }
}

[levjj]

It might be possible to add a flag/option to enable parsing comments that include pre-, postconditions, etc. Currently, "requires", "ensures", etc. are pseudo-function calls that are already exempt from execution and essentially serve as comments with better syntax highlighting and variable scoping.