Skip to content

GitLab

why3
why3
Closed
Opened by GARCHERY Quentin@qgarcherDeveloper

Giving names to requires and ensures

Allow to give names to the pre/post-conditions, for example using the syntax :

requires arg_pos { x > 0 }

This would be helpful because :

  • it would make it clear where this axiom comes from when proving VCs
  • it would make the proof more robust as the axiom name would not change from H12 to H13 when adding another requires
Edited by GARCHERY Quentin
To upload designs, you'll need to enable LFS and have admin enable hashed storage. More information