La logique de hoare, ça sert ?

La logique de hoare, ça sert ? - Algo - Programmation

Marsh Posté le 25-11-2002 à 00:56:20    

Cf. title
 
Je ne suis pas convaincu personnellement, alors faites moi part de vos exp perso.
 
++


---------------
[:roco] Un chtit café et hop ça repart !
Reply

Marsh Posté le 25-11-2002 à 00:56:20   

Reply

Marsh Posté le 25-11-2002 à 07:47:52    

Roco a écrit a écrit :

Cf. title
 
Je ne suis pas convaincu personnellement, alors faites moi part de vos exp perso.
 
++




 
c'est encore un truc à la con de sodomites matheus ou de putains de "neuneu-théroriciens" qui sont incapables d'ecrire un programme (meme en ADA). J'ai un prof comme ca.


---------------
du bon usage de rand [C] / [C++]
Reply

Marsh Posté le 25-11-2002 à 16:40:29    

Juste par curiosité, c'est quoi la logique de hoare ? :??:


---------------
"I wonder if the internal negative pressure in self pumping toothpaste tubes is adjusted for different market altitudes." John Carmack
Reply

Marsh Posté le 25-11-2002 à 18:21:39    

google powaaa, je pense...
 
ben en gros c écrire un algo de facon mathématiques afin de pouvoir le "prouver"
 
enfin c un peu dur a expliquer en 2 lignes, donc une ptite recherche s'impose...


---------------
[:roco] Un chtit café et hop ça repart !
Reply

Marsh Posté le 25-11-2002 à 18:32:24    

Roco a écrit a écrit :

google powaaa, je pense...
 
ben en gros c écrire un algo de facon mathématiques afin de pouvoir le "prouver"
 
enfin c un peu dur a expliquer en 2 lignes, donc une ptite recherche s'impose...



OK merci, j'avais la flemme de chercher (je sais, c'est mal). Je connais vaguement et je pense comme taz.
 
 :hello:


---------------
"I wonder if the internal negative pressure in self pumping toothpaste tubes is adjusted for different market altitudes." John Carmack
Reply

Marsh Posté le 25-11-2002 à 21:43:39    

Taz@PPC a écrit a écrit :

 
c'est encore un truc à la con de sodomites matheus ou de putains de "neuneu-théroriciens" qui sont incapables d'ecrire un programme (meme en ADA). J'ai un prof comme ca.




 
ca va toi??
 
LeGreg


---------------
voxel terrain render engine | animation mentor
Reply

Marsh Posté le 25-11-2002 à 23:14:46    

Taz@PPC a écrit a écrit :

 
 
c'est encore un truc à la con de sodomites matheus ou de putains de "neuneu-théroriciens" qui sont incapables d'ecrire un programme (meme en ADA). J'ai un prof comme ca.




C'est sûr qu'il est plus facile de compiler du C, mais encore faut-il que ça donne bien le résultat voulu. Par contre, si un code en Ada compile sans erreur, il y a de fortes chances qu'on obtienne le résultat voulu.

Reply

Marsh Posté le 25-11-2002 à 23:20:35    

:heink: oui est alors? je comrpends pas ta réflexion?


---------------
du bon usage de rand [C] / [C++]
Reply

Marsh Posté le 25-11-2002 à 23:28:50    

Taz@PPC a écrit a écrit :

 :heink: oui est alors? je comrpends pas ta réflexion?




Tu avais un peu l'air de dénigrer Ada, et moi Ada c'est mon dada...

Reply

Marsh Posté le 25-11-2002 à 23:56:30    

mareek a écrit a écrit :

Je connais vaguement et je pense comme taz.




 
C'est bizarre..
c'est pas une oxymore, ca?
 
"je ne connais pas Bidule mais je pense honnetement que c'est un truc pour sodomite matheux" ?  
 
LeGreg


---------------
voxel terrain render engine | animation mentor
Reply

Marsh Posté le 25-11-2002 à 23:56:30   

Reply

Marsh Posté le 25-11-2002 à 23:58:14    

ben j'ai rien contre mais rien que la synthaxe me rebute (trop trop trop lourdingue)
 
Quand a son approche des differents modèles de programmation et paradigmes, j'aime pas (par exemple: quelle idée de faire du du out du in/out (je sais comment ca fonctionne, mais j'aime pas))
 
je suis fait pour le C et le C++ c'est tout.
 
et je suis toujours assez pété de rire quand on me présente un langage comme puissant par ce que ces compilos donnent du code performant
 
GNAT ptdr....
 
 
sinon rien contre le ADA, je suis obligé d'en faire et ca me fait bien chier.
 
bref je préfère le C et le C++, je suis plus productif avec et ca me semble plus utile dans le monde professionnel.
 
edit:
 
et puis les seuls programmeurs ADA que je connais n'ont jamais fait que ça et ce sont des idiots finis à l'urine incappable de faire autre chose que leur putain de langage à la mort moi le noeud begin/end/endloop/null. Alors j'associe vite...


Message édité par Taz@PPC le 26-11-2002 à 00:01:23

---------------
du bon usage de rand [C] / [C++]
Reply

Marsh Posté le 26-11-2002 à 00:10:02    

legreg a écrit a écrit :

 
 
C'est bizarre..
c'est pas une oxymore, ca?
 
"je ne connais pas Bidule mais je pense honnetement que c'est un truc pour sodomite matheux" ?  
 
LeGreg




Citation :

Vaguement adv. de façon vague, imprécise.


 
en gros, j'en ai entendu parler, je vois à peu prés ce que c'est et je trouve que ça n'a d'intéret que dans le milieu de la recherche qui est plein de gens qui programment comme des pieds en dehors de leur algo chérie de la mort qui tue.
 
Le terme de sodomites matheux est peut être un peu éxagéré (même s'il me fait beaucoup rire), mais je suis d'accord avec TAZ


---------------
"I wonder if the internal negative pressure in self pumping toothpaste tubes is adjusted for different market altitudes." John Carmack
Reply

Marsh Posté le 26-11-2002 à 00:17:53    

mareek a écrit a écrit :

 
en gros, j'en ai entendu parler, je vois à peu prés ce que c'est et je trouve que ça n'a d'intéret que dans le milieu de la recherche qui est plein de gens qui programment comme des pieds en dehors de leur algo chérie de la mort qui tue.




 
on ne doit pas connaitre les memes chercheurs
parce que ceux que je connais sont d'excellents
programmeurs (meme si les meilleurs font de la recherche dans
le prive malheureusement.. enfin ca n'enleve rien a leurs qualites)
 
Bref c'est pas les gens qui frequentent ce forum qui vont leur apprendre a programmer :)
 
LeGreg


---------------
voxel terrain render engine | animation mentor
Reply

Marsh Posté le 26-11-2002 à 00:21:46    

Taz@PPC a écrit a écrit :

 
et puis les seuls programmeurs ADA que je connais n'ont jamais fait que ça et ce sont des idiots finis à l'urine incappable de faire autre chose que leur putain de langage à la mort moi le noeud begin/end/endloop/null. Alors j'associe vite...




Ils ont juste réussit à lancer des fusées dans l'espace ou faire voler des avions...  :kaola:

Reply

Marsh Posté le 26-11-2002 à 00:25:31    

charly007 a écrit a écrit :

 
Ils ont juste réussit à lancer des fusées dans l'espace ou faire voler des avions...  :kaola:  



Ils ont aussi réussi à faire exploser Ariane 5  :whistle:


---------------
"I wonder if the internal negative pressure in self pumping toothpaste tubes is adjusted for different market altitudes." John Carmack
Reply

Marsh Posté le 26-11-2002 à 19:27:39    

mareek a écrit a écrit :

Ils ont aussi réussi à faire exploser Ariane 5  :whistle:  



et t imagine avec du C ? ils auraient fait exploser tous les arianes et fait cracher tous les avions.
car des programmeurs en C qui programment comme des pieds j en connais bcp.
le plus dur en C c'est de l ecrire correctement.


---------------
"PAR LE POUVOIR DU CRÂNE ANCESTRAL, JE DETIENS LA FORCE TOUTE PUISSANTE".
Reply

Marsh Posté le 26-11-2002 à 19:42:25    

oh, le joli topic :o

Reply

Marsh Posté le 26-11-2002 à 20:27:32    

Clarkent a écrit a écrit :

et t imagine avec du C ? ils auraient fait exploser tous les arianes et fait cracher tous les avions.
car des programmeurs en C qui programment comme des pieds j en connais bcp.
le plus dur en C c'est de l ecrire correctement.



mon post était un troll humoristique, c'est sûr qu'en C ariane n'aurait même pas décollé.
 
[:linuxine]


---------------
"I wonder if the internal negative pressure in self pumping toothpaste tubes is adjusted for different market altitudes." John Carmack
Reply

Marsh Posté le 26-11-2002 à 22:21:57    

trouve sur Google, la reponse d'Eiffel  
a Ariane :)
 
http://www.irisa.fr/pampa/EPEE/Ariane5.html
 
LeGreg


---------------
voxel terrain render engine | animation mentor
Reply

Marsh Posté le 26-11-2002 à 22:33:08    

mais arrétez avec le C, c'est aps parce que vous arrivez pas a bien gérer les pointeurs que c'est forcément nul


---------------
du bon usage de rand [C] / [C++]
Reply

Marsh Posté le 26-11-2002 à 22:44:07    

Taz@PPC a écrit a écrit :

mais arrétez avec le C, c'est aps parce que vous arrivez pas a bien gérer les pointeurs que c'est forcément nul




 
C'est le fait que l'on en soit encore à gérer les pointeur qui est nul.  
 
Et pourquoi pas se taper la gestion de la segmentation à la main tant que l'on y est  :kaola:


---------------
brisez les rêves des gens, il en restera toujours quelque chose...  -- laissez moi troller sur discu !
Reply

Marsh Posté le 26-11-2002 à 22:45:28    

faut savoir ce qu'on veut aussi...


---------------
du bon usage de rand [C] / [C++]
Reply

Marsh Posté le 26-11-2002 à 22:46:44    

Roco a écrit a écrit :

Cf. title
 
Je ne suis pas convaincu personnellement, alors faites moi part de vos exp perso.
 
++




 
ca m'a servi a avoir 3 au partiels, mais sinon c'est bien tout :D

Reply

Marsh Posté le 26-11-2002 à 23:19:37    

Roco a écrit a écrit :

google powaaa, je pense...
 
ben en gros c écrire un algo de facon mathématiques afin de pouvoir le "prouver"
 
enfin c un peu dur a expliquer en 2 lignes, donc une ptite recherche s'impose...




Oui ben moi j'écris le programme direct et si y'a pas de coredump ça prouve mon algo :D ...

Reply

Marsh Posté le 26-11-2002 à 23:22:23    

Taz@PPC a écrit a écrit :

mais arrétez avec le C, c'est aps parce que vous arrivez pas a bien gérer les pointeurs que c'est forcément nul




Parfaitement, au moins avec le language C ont détecte très rapidement le bon du mauvais programmeur :D

Reply

Marsh Posté le 26-11-2002 à 23:22:33    

Taz@PPC a écrit a écrit :

mais arrétez avec le C, c'est aps parce que vous arrivez pas a bien gérer les pointeurs que c'est forcément nul




Heu, je ne veux pas remettre ça, mais il y a aussi les pointeurs en Ada (et d'ailleurs je n'arrive pas bien à les gérer !)

Reply

Marsh Posté le 26-11-2002 à 23:26:52    

Taz@PPC a écrit a écrit :

faut savoir ce qu'on veut aussi...




 
ben oui faut savoir ce qu'on veut justement.
 
Ici on programme pour des jeux videos donc si ca plante, si on droppe une frame au milieu ou si la physique a des defauts a 2 decimales apres la virgule ca ne cause pas mort d'homme (enfin peut etre sur Counter Strike en reseau :D ). donc on peut se permettre de tout coder en C++ avec de l'assembleur au milieu. Meme ca ne nous empeche pas d'avoir des methodes d'ingenierie strictes (tests de regression, generateur de code, chasse au code C-Sale (cast, prise en compte de la constness) etc..).
 
Par contre sur des logiciels qui dirigent des fusees et plus encore ou il y a des vies humaines en jeu (avions etc..)
difficile de justifier de faire joujou avec les pointeurs, genre "regardez, je charge mes donnees en une fois et je rajoute un offset aux emplacements x et y, de toute facon j'ai precise un pack de 1 sur mes structures, donc ca peut pas planter sauf sur processeur 64 bits.. eheh je n'ai aucun moyen de verifier que ca marche sauf en lancant le truc plusieurs fois et de prier pour que j'ai teste tous les cas.."
 
LeGreg


---------------
voxel terrain render engine | animation mentor
Reply

Marsh Posté le 26-11-2002 à 23:28:16    

ada, que de la balle, meme pas de [] pour les tableaux. et si ton tapes dans un movais indice: rien , pas de plantage ni de erreur de segmentation, el programme quitte normalement. c tout de suite plus facile pour trouver les erreurs


---------------
du bon usage de rand [C] / [C++]
Reply

Marsh Posté le 26-11-2002 à 23:28:49    

legreg a écrit a écrit :

 
Par contre sur des logiciels qui dirigent des fusees et plus encore ou il y a des vies humaines en jeu (avions etc..)




 
Si tu savais... quand je vois comment ca se passe dans un hopital, c'est effrayant, y'a même pas de tests de non regression, alors que c'est vraiment le minimum :/

Reply

Marsh Posté le 26-11-2002 à 23:38:58    

darkoli a écrit a écrit :

 
Parfaitement, au moins avec le language C ont détecte très rapidement le bon du mauvais programmeur :D



sauf qu on aimerait bien le det'ecter avant de depenser des milliards de dollars :sol:.
 
et le C c est proche du langage machine, un niveau au dessus, ca n a d onc rien a voir avec du c++ ada et consort qui sont encore aun niveau au dessus.
 
le C est tellement permissif qu il permet aussi de faire des conneries.
 
et que ceux qui pretendent maitriser le C en l ayant appris a l ecole leve le doigt, car j'aime bien rire parfois :lol:.


Message édité par Clarkent le 26-11-2002 à 23:40:54

---------------
"PAR LE POUVOIR DU CRÂNE ANCESTRAL, JE DETIENS LA FORCE TOUTE PUISSANTE".
Reply

Marsh Posté le 26-11-2002 à 23:43:42    

darkoli a écrit a écrit :

 
Parfaitement, au moins avec le language C ont détecte très rapidement le bon du mauvais programmeur :D




 
chui d'accord, beaucoup d'enseignement du C sont complètement nul (que ce soit des professeurs ou des manuels) et apres on a des mauvais programmeurs qui s'ignorent...


---------------
du bon usage de rand [C] / [C++]
Reply

Marsh Posté le 26-11-2002 à 23:48:19    

Clarkent a écrit a écrit :

sauf qu on aimerait bien le det'ecter avant de depenser des milliards de dollars :sol:.
 
et le C c est proche du langage machine, un niveau au dessus, ca n a d onc rien a voir avec du c++ ada et consort qui sont encore aun niveau au dessus.
 
le C est tellement permissif qu il permet aussi de faire des conneries.
 
et que ceux qui pretendent maitriser le C en l ayant appris a l ecole leve le doigt, car j'aime bien rire parfois :lol:.




Je suis d'accord.
J'ai fait du C pour la première fois en 1996 (DUT) et j'en fais toujours depuis et "j'apprends "encore des trucs aujourd'hui pas tellement sur le language en lui-même mais plutôt sur la façon de l'utiliser et d'avoir des programmes fiables :D. Et je dois dire que je suis plutôt content du résultat mais je ne suis pas le seul à faire les développements et parfois je vois de ces horreurs :cry:.

Reply

Marsh Posté le 26-11-2002 à 23:50:58    

Clarkent a écrit a écrit :

 
et que ceux qui pretendent maitriser le C en l ayant appris a l ecole leve le doigt, car j'aime bien rire parfois :lol:.




 
j'ai appris le C a l'ecole :)
 
[Off Topic]
je ne pretends pas le maitriser (encore moins le C++)
mais j'en avais appris assez pour coder un proxy multithread
(avec cache et suppression des pubs) :)
Et pour un premier programme il etait suffisamment portable pour etre porte de Linux a UltraSparc en quelques jours (a cause des differentes merdes sur la gestion des threads et des messages..)  
[/OT]
 
LeGreg


---------------
voxel terrain render engine | animation mentor
Reply

Marsh Posté le 26-11-2002 à 23:59:36    

Taz@PPC a écrit a écrit :

 
 
c'est encore un truc à la con de sodomites matheus ou de putains de "neuneu-théroriciens" qui sont incapables d'ecrire un programme (meme en ADA). J'ai un prof comme ca.




 
pas d'accord
il fo bien des matheux et des theoriciens pour savoir si l'algo est valide et calculer son cout.
 
tu va me dire: mais c pareil si on les essai...
 
ben non... sur les algo de tri par exemple, on utilise pas le meme si ya plus ou moins de 4 elements, etc...


---------------
"Je brandirai une épée d'orichalque, je m'assouvirai sur des Templiers." | "Avec dans son sillage l'Ombre du Diable, Leirn appelait les morts pour une danse macabre et déchainaît les horreurs de la nuit..."
Reply

Marsh Posté le 27-11-2002 à 00:14:19    

leirn a écrit a écrit :

 
 
pas d'accord
il fo bien des matheux et des theoriciens pour savoir si l'algo est valide et calculer son cout.
 
tu va me dire: mais c pareil si on les essai...
 
ben non... sur les algo de tri par exemple, on utilise pas le meme si ya plus ou moins de 4 elements, etc...



non mais il croit que sur ungros projet on va tout faire comme ca puis apres on va essayer savoir si ca marche :D, on reflechit pas a faire le moins d erreur possible :D.


Message édité par Clarkent le 27-11-2002 à 00:14:27

---------------
"PAR LE POUVOIR DU CRÂNE ANCESTRAL, JE DETIENS LA FORCE TOUTE PUISSANTE".
Reply

Marsh Posté le 27-11-2002 à 00:17:02    

Clarkent a écrit a écrit :

non mais il croit que sur ungros projet on va tout faire comme ca puis apres on va essayer savoir si ca marche :D, on reflechit pas a faire le moins d erreur possible :D.




 
en general on se contente d'une constante de boucle pour valider un algo en plus ...


---------------
"Je brandirai une épée d'orichalque, je m'assouvirai sur des Templiers." | "Avec dans son sillage l'Ombre du Diable, Leirn appelait les morts pour une danse macabre et déchainaît les horreurs de la nuit..."
Reply

Marsh Posté le 27-11-2002 à 00:29:51    

leirn a écrit a écrit :

 
 
en general on se contente d'une constante de boucle pour valider un algo en plus ...



tu veux dire un invariant :D ?


---------------
"PAR LE POUVOIR DU CRÂNE ANCESTRAL, JE DETIENS LA FORCE TOUTE PUISSANTE".
Reply

Marsh Posté le 27-11-2002 à 00:32:52    

La logique de Hoare, c'est un formalisme qui permet de verifier qu'un programme est sans faute logique. C'est pas mal, mais malheureusement c'est assez lourd comme technique [je me souviens que pour montrer qu'une routine d'ecriture fichier etait correcte en logique de Hoare, ça m'a pris 3 pages] et de ce fait, a part en fac et dans des papiers theoriques, je connais pas vraiment d'emploi.
A+,


Message édité par gilou le 27-11-2002 à 00:33:59

---------------
There's more than what can be linked! --    Iyashikei Anime Forever!    --  AngularJS c'est un framework d'engulé!  --
Reply

Marsh Posté le 27-11-2002 à 00:45:09    

gilou a écrit a écrit :

La logique de Hoare, c'est un formalisme qui permet de verifier qu'un programme est sans faute logique. C'est pas mal, mais malheureusement c'est assez lourd comme technique [je me souviens que pour montrer qu'une routine d'ecriture fichier etait correcte en logique de Hoare, ça m'a pris 3 pages] et de ce fait, a part en fac et dans des papiers theoriques, je connais pas vraiment d'emploi.
A+,




 
 :jap:


---------------
[:roco] Un chtit café et hop ça repart !
Reply

Marsh Posté le 27-11-2002 à 00:45:19    

gilou a écrit a écrit :

La logique de Hoare, c'est un formalisme qui permet de verifier qu'un programme est sans faute logique. C'est pas mal, mais malheureusement c'est assez lourd comme technique [je me souviens que pour montrer qu'une routine d'ecriture fichier etait correcte en logique de Hoare, ça m'a pris 3 pages] et de ce fait, a part en fac et dans des papiers theoriques, je connais pas vraiment d'emploi.
A+,



c'est un truc à la con de sodomites matheus en somme  :whistle:  
 
 
(humour)


---------------
"I wonder if the internal negative pressure in self pumping toothpaste tubes is adjusted for different market altitudes." John Carmack
Reply

Marsh Posté le    

Reply

Sujets relatifs:

Leave a Replay

Make sure you enter the(*)required information where indicate.HTML code is not allowed