Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • why3 why3
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Graph
    • Compare
  • Issues 166
    • Issues 166
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 26
    • Merge requests 26
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar

La mise à jour du service Gitlab est terminée. Merci aux collègues du service de production de la DSI qui ont réalisé cette opération qui outre les aspects évolution du logiciel nous a permis de faire le nécessaire face à des failles de sécurité.
Les principales releases notes concernant cette montée de version sont disponibles ici :
https://about.gitlab.com/releases/2023/01/22/gitlab-15-8-released/
https://about.gitlab.com/releases/2022/12/22/gitlab-15-7-released/
https://about.gitlab.com/releases/2022/11/22/gitlab-15-6-released/

  • Why3Why3
  • why3why3
  • Issues
  • #136
Closed
Open
Issue created Jun 15, 2018 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
Assignee
Assign to
Time tracking