Bonjour, je cherche quelqu’un d’expérimenté ou du moins connaisseur dans le domaine de logique et de la sémantique des langages plus spécialement la sémantique axiomatique.

Bonjour,

Alors c'est un peu compliqué de te répondre. Il faudrait préciser à quel point tu en es en sémantique (les cours que tu as suivi, ton niveau d'étude, etc...), parce que la notion de conaisseur est relative.

J'ai des notions, mais de là à dire que ne suis conaisseur, non.

Sinon, peux-tu exposer ton problème parce que là, personne ne peux t'aider.

Je suis master 1 en System d'information reparti et j'ai la semaine prochaine un examen de sémantique de langage et je trouve des difficultés a comprendre certains points comme démontrer la validité d'un triplet {a}c{b},

trouver l'invariant d'une boucle while, son post et pré-condition et Annoter un programme

et calculer la fiabilité d'une précondition avec un WP.

merci.

Ok je vois.

Il y a toujours plusieurs niveaux à ça.

Mais en gros :

Pour montrer qu'un programme est juste, il y a deux choses à montrer :

 - la terminaison : il faut montrer que s'il y a des boucles while ou des fonctions récursives, elles terminent. On peut utiliser un variant de boucle pour ça

 - la correction partielle : on utilise généralement un trriplet de Haore. Un triplet de Haore, c'est dire : si j'ai telle précondition et que ça termine, alors mon programme fait ce que je veux (ce que le triplet dit). La précondition, ça va être toutes les contraintes sur l'entrée. La post-condition, ça va être le résultat du programme en fonction de l'entrée Pour montrer que le triplet est valide, on part de l'entrée (c'est une formule logique) et on annote le programme ligne par ligne, en appliquant les règles du système de preuve de Haore. Si à la fin du programme tu as la post-condition, c'est gagné.

Je te met  un lien vers un cours qui explique ça un peu mieux que moi et plus en détails : p 16-24 http://www.lsv.fr/~haddad/transparents-Algorithmique.pdf

Il y a des exemples d'annotation de programmes et de triplets.

A part te donner des exemples, je ne vois pas quoi faire car il n'y a pas de méthode canonique pour trouver un invariant, etc.. il faut comprendre le programme et voir ce que l'on veut.