Bonjour !

Voila j´ai une question qui m´intrigue franchement, le langage B et la methode de specification en B, c´est la meme chose ou c´est totalement diferent ?

Est-ce que quelqu´un a une idée ?

le langage B ? Tu veux parler du langage précédant le langage C de Kernighan et Ritchie ? Je savais pas que des formes d´êtres vivants s´interessaient encore à ça...

MOUARF !

Non mais en fait je fais des etudes d´infos et j´apprend un " langage de specification" qui s´appelle B ( d´ailleur c´est tres chiant ! ) et en me balandant sur le net j´ai vu qu´il existait un langage B qui justement comme tu dis précédait le langage C. Je trouve ca bizarre que 2 langagent portent le meme nom c´est tout...

Bah il y a tellement de langage différent . .. et dans notre société-de-zombiS-sans-imagination . ..

Kali> On joue les originaux ? Tu codes en quoi ?

bein des trucs de profs de fac ça, de nous faire apprendre des trucs inutiles...
Bon courage pour le langage " B"

Le 19 décembre 2004 à 19:24:35 JeanYvesYves a écrit :
bein des trucs de profs de fac ça, de nous faire apprendre des trucs inutiles...
Bon courage pour le langage " B"

Oui, apprendre le fonctionnement d'un langage de spec c'est inutile.

Tiens, c'est le langage qui a servi à vérifier formellement les lignes de métro 1 et 14 à Paris. Rien à voir avec l'ancêtre du C apparemment. Je me demande pourquoi ce nom.

Joli up par contre

Je ne sais déjà pas ce que c'est qu'un raffinement...

La méthode B c'est un truc de niche tu trouveras pas ici et encore moins sans politesse, sans décrire ton problème et sans montrer ton avancée dans le travail, on va pas s'amuser à faire ton TP.

Je l'ai fait à mon semestre dernier mais c'était tellement chiant à mourir que j'ai même pas envie de replonger dedans.

Et sinon pour les autres, je pense pas que son UV concerne la méthode B comme outil technique mais plutôt une découverte des méthodes formelles pour faire des logiciels critiques.

merci chcolayte, pour ton envie de m'aider, parce que vraiment j'ai pas compris quoi faire pour le raffinement de cette machine abstraite.le raffinement consiste à ajouter des nouveaux variables concrètes et les introduire dans l'invariant et dans les opérations, à condition ne pas modifier ces dernières.et je vois que cette machine est concrète et n'a pas besoin d'un raffinement, mais l'énoncé de cette exercice demande le raffinement et l'implémentation de cette machine.
svp y'a quelqun qui m'aide ou me guide pour un forum utile?
merci .

Le 26 décembre 2019 à 12:31:30 rose16 a écrit :

vraiment j'ai pas compris quoi faire pour le raffinement de cette machine abstraite.le raffinement consiste à ajouter des nouveaux variables concrètes et les introduire dans l'invariant et dans les opérations, à condition ne pas modifier ces dernières.et je vois que cette machine est concrète et n'a pas besoin d'un raffinement, mais l'énoncé de cette exercice demande le raffinement et l'implémentation de cette machine.

svp y'a quelqun qui m'aide
merci .

la machine abstraite:
MACHINE
DISTRIBUTEUR
CONSTANTS
Prix ,
Valeur-pièce
PROPERTIES
Prix ∈ NAT ˄ Valeur-pièce ∈ NAT
˄ Prix mod Valeur-pièce = 0
VARIABLES
Somme-versée,
Nb-demandes,
Nb-disponibles
INVARIANT
Somme-versée ∈ NAT ˄
Nb-demandes ∈ NAT ˄
Nb-disponibles ∈ NAT ˄
Nb demandes < Nb disponibles ˄
Somme-versée <= (Nb-demandes  Prix)
INITIALISATION
BEGIN
Somme-versée := 0 ||
Nb-demandes := 0 ||
Nb-disponibles ∈ NAT
END
OPERATIONS
Indiquer_nbre (nbc ) = PRE nbc ∈ NAT1 ˄ nbc < Nb-disponibles ˄
Somme-versée = 0 ˄ Nb demandes = 0
THEN
Nb demandes := nbc
END ;
Introduire_piece = PRE Nb-demandes > 0 ˄
Somme-versée + Valeur-pièce <= Nb demandes  Prix
THEN
Somme-versée := Somme-versée + Valeur-pièce
END ;
Distribuer = PRE Somme-versée = Nb-demandes  Prix THEN
Somme-versée := 0 ||
Nb-disponibles := Nb-disponibles – Nb-demandes ||
Nb-demandes := 0
END ;
rendu  Annuler = BEGIN
Somme-versée := 0 || Nb-demandes := 0 || rendu := Somme-versée
END
END

Le 26 décembre 2019 à 18:55:53 rose16 a écrit :

Le 26 décembre 2019 à 12:31:30 rose16 a écrit :

vraiment j'ai pas compris quoi faire pour le raffinement de cette machine abstraite.le raffinement consiste à ajouter des nouveaux variables concrètes et les introduire dans l'invariant et dans les opérations, à condition ne pas modifier ces dernières.et je vois que cette machine est concrète et n'a pas besoin d'un raffinement, mais l'énoncé de cette exercice demande le raffinement et l'implémentation de cette machine.

svp y'a quelqun qui m'aide
merci .

la machine abstraite:
MACHINE
DISTRIBUTEUR
CONSTANTS
Prix ,
Valeur-pièce
PROPERTIES
Prix ∈ NAT ˄ Valeur-pièce ∈ NAT
˄ Prix mod Valeur-pièce = 0
VARIABLES
Somme-versée,
Nb-demandes,
Nb-disponibles
INVARIANT
Somme-versée ∈ NAT ˄
Nb-demandes ∈ NAT ˄
Nb-disponibles ∈ NAT ˄
Nb demandes < Nb disponibles ˄
Somme-versée <= (Nb-demandes  Prix)
INITIALISATION
BEGIN
Somme-versée := 0 ||
Nb-demandes := 0 ||
Nb-disponibles ∈ NAT
END
OPERATIONS
Indiquer_nbre (nbc ) = PRE nbc ∈ NAT1 ˄ nbc < Nb-disponibles ˄
Somme-versée = 0 ˄ Nb demandes = 0
THEN
Nb demandes := nbc
END ;
Introduire_piece = PRE Nb-demandes > 0 ˄
Somme-versée + Valeur-pièce <= Nb demandes  Prix
THEN
Somme-versée := Somme-versée + Valeur-pièce
END ;
Distribuer = PRE Somme-versée = Nb-demandes  Prix THEN
Somme-versée := 0 ||
Nb-disponibles := Nb-disponibles – Nb-demandes ||
Nb-demandes := 0
END ;
rendu  Annuler = BEGIN
Somme-versée := 0 || Nb-demandes := 0 || rendu := Somme-versée
END
END

Le 30 décembre 2019 à 18:15:07 rose16 a écrit :

Le 26 décembre 2019 à 18:55:53 rose16 a écrit :

Le 26 décembre 2019 à 12:31:30 rose16 a écrit :

vraiment j'ai pas compris quoi faire pour le raffinement de cette machine abstraite.le raffinement consiste à ajouter des nouveaux variables concrètes et les introduire dans l'invariant et dans les opérations, à condition ne pas modifier ces dernières.et je vois que cette machine est concrète et n'a pas besoin d'un raffinement, mais l'énoncé de cette exercice demande le raffinement et l'implémentation de cette machine.

svp y'a quelqun qui m'aide
merci .

la machine abstraite:
MACHINE
DISTRIBUTEUR
CONSTANTS
Prix ,
Valeur-pièce
PROPERTIES
Prix ∈ NAT ˄ Valeur-pièce ∈ NAT
˄ Prix mod Valeur-pièce = 0
VARIABLES
Somme-versée,
Nb-demandes,
Nb-disponibles
INVARIANT
Somme-versée ∈ NAT ˄
Nb-demandes ∈ NAT ˄
Nb-disponibles ∈ NAT ˄
Nb demandes < Nb disponibles ˄
Somme-versée <= (Nb-demandes  Prix)
INITIALISATION
BEGIN
Somme-versée := 0 ||
Nb-demandes := 0 ||
Nb-disponibles ∈ NAT
END
OPERATIONS
Indiquer_nbre (nbc ) = PRE nbc ∈ NAT1 ˄ nbc < Nb-disponibles ˄
Somme-versée = 0 ˄ Nb demandes = 0
THEN
Nb demandes := nbc
END ;
Introduire_piece = PRE Nb-demandes > 0 ˄
Somme-versée + Valeur-pièce <= Nb demandes  Prix
THEN
Somme-versée := Somme-versée + Valeur-pièce
END ;
Distribuer = PRE Somme-versée = Nb-demandes  Prix THEN
Somme-versée := 0 ||
Nb-disponibles := Nb-disponibles – Nb-demandes ||
Nb-demandes := 0
END ;
rendu  Annuler = BEGIN
Somme-versée := 0 || Nb-demandes := 0 || rendu := Somme-versée
END
END

Dans ma fac, on a vite fait du simili méthode (le prof disait atelier pas méthode) B sur papier mais nos TPs machine étaient en Coq. Ca me manque pas cette UE

merci TechnoForce3, tu as raison la méthode s'appel B et l'outil s'appel Atelier B

MDR la preuve formel en B ou autre c’est justement l’avenir . Ce qui est complètement inutile c’est écrire des tests unitaires qui assurent pas du tout que le prog fonctionne. Un mec qui écrit des tests c’est un peu comme le médecin du moyen âge qui charcutait ses patients à vue d’œil. Alors qu’un médecin moderne qui touche même pas au patient et qui le guérit de façon non intrusive c’est comme le programmeur qui donne la garantie que son prog est 100% correct.

Le 04 janvier 2020 à 20:39:30 infireman a écrit :
MDR la preuve formel en B ou autre c’est justement l’avenir . Ce qui est complètement inutile c’est écrire des tests unitaires qui assurent pas du tout que le prog fonctionne. Un mec qui écrit des tests c’est un peu comme le médecin du moyen âge qui charcutait ses patients à vue d’œil. Alors qu’un médecin moderne qui touche même pas au patient et qui le guérit de façon non intrusive c’est comme le programmeur qui donne la garantie que son prog est 100% correct.

Sauf que pour 99% des cas c'est overkill. Ça prends beaucoup plus de temps et d'argent de faire ce genre de programmes, si c'était rentable, toutes les entreprises l'utiliserais sauf que ce n'est pas le cas. En plus, le programme ne reste pas 100% safe, dans certains cas, on doit laisser certains cas en B et implémenter les vérifs plus tard dans l'implémentation en C (évoqué par mon professeur qui a participé au programme qui tourne sur une ligne de métro)