La logique de hoare, ça sert ? - Algo - Programmation
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.
Marsh Posté le 25-11-2002 à 16:40:29
Juste par curiosité, c'est quoi la logique de hoare ?
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...
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.
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
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.
Marsh Posté le 25-11-2002 à 23:28:50
Taz@PPC a écrit a écrit : 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...
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
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...
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
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
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...
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... |
Ils ont aussi réussi à faire exploser Ariane 5
Marsh Posté le 26-11-2002 à 19:27:39
mareek a écrit a écrit : Ils ont aussi réussi à faire exploser Ariane 5 |
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.
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é.
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
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
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
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 ...
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
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 !)
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 ). 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
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
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
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 |
sauf qu on aimerait bien le det'ecter avant de depenser des milliards de dollars .
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 .
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 |
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...
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 . 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 . |
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 . 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 .
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 . |
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
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...
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 , on reflechit pas a faire le moins d erreur possible .
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 , on reflechit pas a faire le moins d erreur possible . |
en general on se contente d'une constante de boucle pour valider un algo en plus ...
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 ?
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+,
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+, |
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
(humour)
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 !