Et voilà, quand on fait des commentaires en béotien, on tombe à côté :-)
Ce n'est probablement pas lié à la définition de SPARK himself, mais je crois que gnatprove utilise Why3.
Je ne comprends pas ce que cela implique, mais comme tu l'as associé à la logique de Hoare dans ton intro, ça semble confirmer.
[^] # Re: Pour la complétude, j'ajoute le couple SPARK/Ada
Posté par Lionel Draghi (site web personnel) . En réponse à la dépêche Programmer des démonstrations : une modeste invitation aux assistants de preuve. Évalué à 1.
Et voilà, quand on fait des commentaires en béotien, on tombe à côté :-)
Ce n'est probablement pas lié à la définition de SPARK himself, mais je crois que gnatprove utilise Why3.
Je ne comprends pas ce que cela implique, mais comme tu l'as associé à la logique de Hoare dans ton intro, ça semble confirmer.