Skip to content

GitLab

Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Closed
Created by Guillaume Melquiond@melquionOwner

Make `any ... ensures` less error-prone

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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information