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
toH13
when adding anotherrequires