GitLab

I didn't know that any ... ensures introduces an axiom. And I was not the only developer to get it wrong. We really should limit the number of language constructions that introduce axioms.

There are only three occurrences of this construction in the gallery:

• unraveling_a_card_trick: any int ensures { 0 <= result <= n*m }
• white_and_black_balls: any (x: int, y: int) ensures { 0 <= x && 0 <= y && x + y = 2 && x <= !b && y <= !w }
• vstte12_bfs: any B.t ensures { !!result = succ v }

The first two occurrences are actually provable, so I am not sure their authors intended them to generate axioms. The last one is an actual axiom, but it should ideally have been val, so that the user could instantiate it to obtain an effective algorithm.

Thus, I suggest that this construction be repurposed so that it generates a verification condition.