Discussion :

[Invité]

Bonjour à tous.

Je suis débutant, mon but est d'apprendre à écrire une spécification formelle et à l'implémenter. (je m'intéresse uniquement aux spécifications fonctionnelles, les plus abstraites possibles, pour débuter)

On m'as dit que les grands types de langages de spécifications formelles sont :

- logique des prédicats
- langage de flots de données (synchrones) qui ont des opérateurs temporels
- automates

Et, plus controversé, quelques langages de haut niveau peuvent servir à faire de la spéc. formelle :

- prolog
- fonctionnel pure genre haskell
- quelques langages procéduraux genre Abstract State Machine

Je suis en train d'essayer de lire un bouquin sur la méthode B, mais je suis noyé par les détails, ça me décourage un peu car je ne suis même pas sur que cette méthode corresponde à ce que je veux faire.

Je voudrais juste décrire un programme simple avec un langage formel, prouver à la main une ou deux propriétés du programme à partir des spécifications abstraites, puis implémenter le programme.

Avez-vous une idée d'un langage formel que je pourrais employer pour mon initiation ? (juste comprendre en gros qu'est ce que c'est les spéc. formelles)

Merci pour votre aide

[Pouic]

Le langage B, ou, dans un autre registre, des langages comme Esterel ou Lustre, ou encore SPIN te permettront d'exprimer certaines exigences, et de faire un lien avec l'implantation.

D'autres méthodes formelles te permettront d'exprimer les exigences avec davantage de souplesse, mais tu devras gérer "à la main" le fait que ton code ne découle pas directement de ta spécification