Ca ne va pas compléter la pyramide animale des musiciens de Brême, ni contribuer à ce très intéressant état de l'art mathématique sur le sujet, mais pour l'anecdote j'ajoute l'exemple de la spécification de la procedure Swap avec le prouveur SPARK et le langage Ada :
Intéressant au passage de voir comment la syntaxe des langages, en utilisant plus ou moins de symboles, se destine plus à des mathématiciens ou à des (削除) béotiens (削除ここまで) informaticiens.
PS1 : je ne fais pas partie des spécialistes de SPARK
PS2 : je fais partie des béotiens :-)
# 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é à 3.
Ca ne va pas compléter la pyramide animale des musiciens de Brême, ni contribuer à ce très intéressant état de l'art mathématique sur le sujet, mais pour l'anecdote j'ajoute l'exemple de la spécification de la procedure Swap avec le prouveur SPARK et le langage Ada :
Intéressant au passage de voir comment la syntaxe des langages, en utilisant plus ou moins de symboles, se destine plus à des mathématiciens ou à des
(削除) béotiens (削除ここまで)informaticiens.PS1 : je ne fais pas partie des spécialistes de SPARK
PS2 : je fais partie des béotiens :-)