B方法
点击看大图
定价 ：￥57.00
普通会员 ： ￥51.30
1-3星会员： ￥50.16
4-5星会员： ￥48.45
团购急调缺货预定
促销活动
基本信息
原书名： The B-Book:Assigning Programs to Meanings
原出版社： Cambridge University Press
作者： [美]Jean-Raymond Abrial, J.-R. Abrial [作译者介绍]
译者： 裘宗燕
丛书名： 国外计算机科学教材系列
出版社：电子工业出版社
ISBN：7505393391
上架时间：2004-7-1
出版日期：2004 年6月
开本：16开
页码：526
版次：1-1
jeudi 3 novembre 2011
dimanche 19 juin 2011
Structures de données et méthodes formelles (génie logiciel, méthodes formelles, programmation, algorithmes, mathématiques discrètes, logique, méthode B)
Structures de données et méthodes formelles
Marc Guyomard
Springer, 2011
http://www.springer.com/computer/book/978-2-8178-0199-5
Marc Guyomard
Springer, 2011
http://www.springer.com/computer/book/978-2-8178-0199-5
mardi 30 mars 2010
Décès de Robin Milner
Arthur John Robin Gorell Milner (né le 13 janvier 1934 à Yealmpton, près
de Plymouth et mort le 20 mars 2010 à Cambridge était diplômé de
l'université de Cambridge, il a été professeur aux universités de Londres,
Swansea, Édimbourg, Stanford et Cambridge.
Robin Milner est connu pour ses trois principales contributions en
informatique, à savoir :
* LCF, le premier système de démonstration automatique de théorèmes,
utilisé pour démontrer automatiquement des assertions mathématiques ;
* le langage ML ;
* la théorie d'analyse des systèmes concurrents (calculus of
communicating systems, CCS) et son successeur, le pi-calcul.
Ses trois inventions lui valurent le prix Turing de l'ACM en 1991[3].
http://www.cl.cam.ac.uk/~rm135/
Il était venu faire une conférence à Nantes en 2007.
Il a alimenté mon cours de Spécification Deuxième partie. Son livre
Communication and Concurrency est un petit chef-d'œuvre.
Son dernier livre The Space and Motion of Communicating Agents est paru
chez Cambridge University Press il y a un an.
de Plymouth et mort le 20 mars 2010 à Cambridge était diplômé de
l'université de Cambridge, il a été professeur aux universités de Londres,
Swansea, Édimbourg, Stanford et Cambridge.
Robin Milner est connu pour ses trois principales contributions en
informatique, à savoir :
* LCF, le premier système de démonstration automatique de théorèmes,
utilisé pour démontrer automatiquement des assertions mathématiques ;
* le langage ML ;
* la théorie d'analyse des systèmes concurrents (calculus of
communicating systems, CCS) et son successeur, le pi-calcul.
Ses trois inventions lui valurent le prix Turing de l'ACM en 1991[3].
http://www.cl.cam.ac.uk/~rm135/
Il était venu faire une conférence à Nantes en 2007.
Il a alimenté mon cours de Spécification Deuxième partie. Son livre
Communication and Concurrency est un petit chef-d'œuvre.
Son dernier livre The Space and Motion of Communicating Agents est paru
chez Cambridge University Press il y a un an.
jeudi 11 février 2010
samedi 28 novembre 2009
Qu'est-ce donc que le temps ?
" Qu'est-ce donc que le temps ? Si personne ne me le demande, je le sais : mais que je veuille l'expliquer à la demande, je ne le sais pas ! Et pourtant — je le dis en toute confiance — je sais que si rien ne se passait il n'y aurait pas de temps passé, et si rien n'advenait, il n'y aurait pas d'avenir, et si rien n'existait, il n'y aurait pas de temps présent. Mais ces deux temps, passé et avenir, quel est leur mode d'être alors que le passé n'est plus et que l'avenir n'est pas encore ? Quant au présent, s'il était toujours présent sans passer au passé, il ne serait plus le temps mais l'éternité.
Si donc le présent, pour être du temps, ne devient tel qu'en passant au passé, quel mode d'être lui reconnaître, puisque sa raison d'être est de cesser d'être, si bien que nous pouvons dire que le temps a l'être seulement parce qu'il tend au néant. (...) Enfin, si l'avenir et le passé sont, je veux savoir où ils sont. Si je ne le puis, je sais du moins que, où qu'ils soient, ils n'y sont pas en tant que choses futures ou passées, mais sont choses présentes. Car s'ils y sont, futur il n'y est pas encore, passé il n'y est plus. Où donc qu'ils soient, quels qu'ils soient, ils n'y sont que présents. Quand nous racontons véridiquement le passé, ce qui sort de la mémoire, ce n'est pas la réalité même, la réalité passée, mais des mots, conçus d'après ces images qu'elle a fixées comme des traces dans notre esprit en passant par les sens.
Mon enfance par exemple, qui n'est plus, est dans un passé qui n'est plus, mais quand je me la rappelle et la raconte, c'est son image que je vois dans le présent, image présente en ma mémoire. En va-t-il de même quand on prédit l'avenir ? Les choses qui ne sont pas encore sont-elles pressenties grâce à des images présentes ? Je confesse, mon Dieu, que je ne le sais pas. Mais je sais bien en tout cas que d'ordinaire nous préméditons nos actions futures et que cette préméditation est présente, alors que l'action préméditée n'est pas encore puisqu'elle est à venir. Quand nous l'aurons entreprise, quand nous commencerons d'exécuter notre projet, alors l'action existera mais ne sera plus à venir, mais présente. (...)
Il est dès lors évident et clair que ni l'avenir ni le passé ne sont et qu'il est impropre de dire : il y a trois temps, le passé, le présent, l'avenir, mais qu'il serait exact de dire : il y a trois temps, un présent au sujet du passé, un présent au sujet du présent, un présent au sujet de l'avenir. Il y a en effet dans l'âme ces trois instances, et je ne les vois pas ailleurs : un présent relatif au passé, la mémoire, un présent relatif au présent, la perception, un présent relatif à l'avenir, l'attente. Si l'on me permet ces expressions, ce sont bien trois temps que je vois et je conviens qu'il y en a trois."
Confessions, livre XI. Paragraphe: XIV, XVIII, XX
Si donc le présent, pour être du temps, ne devient tel qu'en passant au passé, quel mode d'être lui reconnaître, puisque sa raison d'être est de cesser d'être, si bien que nous pouvons dire que le temps a l'être seulement parce qu'il tend au néant. (...) Enfin, si l'avenir et le passé sont, je veux savoir où ils sont. Si je ne le puis, je sais du moins que, où qu'ils soient, ils n'y sont pas en tant que choses futures ou passées, mais sont choses présentes. Car s'ils y sont, futur il n'y est pas encore, passé il n'y est plus. Où donc qu'ils soient, quels qu'ils soient, ils n'y sont que présents. Quand nous racontons véridiquement le passé, ce qui sort de la mémoire, ce n'est pas la réalité même, la réalité passée, mais des mots, conçus d'après ces images qu'elle a fixées comme des traces dans notre esprit en passant par les sens.
Mon enfance par exemple, qui n'est plus, est dans un passé qui n'est plus, mais quand je me la rappelle et la raconte, c'est son image que je vois dans le présent, image présente en ma mémoire. En va-t-il de même quand on prédit l'avenir ? Les choses qui ne sont pas encore sont-elles pressenties grâce à des images présentes ? Je confesse, mon Dieu, que je ne le sais pas. Mais je sais bien en tout cas que d'ordinaire nous préméditons nos actions futures et que cette préméditation est présente, alors que l'action préméditée n'est pas encore puisqu'elle est à venir. Quand nous l'aurons entreprise, quand nous commencerons d'exécuter notre projet, alors l'action existera mais ne sera plus à venir, mais présente. (...)
Il est dès lors évident et clair que ni l'avenir ni le passé ne sont et qu'il est impropre de dire : il y a trois temps, le passé, le présent, l'avenir, mais qu'il serait exact de dire : il y a trois temps, un présent au sujet du passé, un présent au sujet du présent, un présent au sujet de l'avenir. Il y a en effet dans l'âme ces trois instances, et je ne les vois pas ailleurs : un présent relatif au passé, la mémoire, un présent relatif au présent, la perception, un présent relatif à l'avenir, l'attente. Si l'on me permet ces expressions, ce sont bien trois temps que je vois et je conviens qu'il y en a trois."
Confessions, livre XI. Paragraphe: XIV, XVIII, XX
dimanche 1 février 2009
lundi 8 septembre 2008
Dur, dur
Anecdote.
Il restait une caisse en haut d'une armoire de mon bureau. Comme une échelle était disponible dans le couloir, j'ai finalement pu descendre cette caisse.
Il y avait des classeurs. Je prends le premier en présence d'un collègue qui lui aussi part à la retraite. Je constate qu'il s'agit d'un dossier de td de spec. Le collègue me dit de ne pas l'ouvrir, sinon ça va me mettre le moral à zéro. J'ouvre cependant.
Très bien écrit, bien structuré, enfin un dossier qui respecte les consignes (à une époque où je ne les écrivais pas et où je ne les énonçais qu'une fois dans l'année), un dossier réutilisable, etc. J'avais noté "TB".
De quand date ce dossier ? De 1998.
J'en prends un deuxième. Encore un dossier comme depuis quelques années je n'en vois plus. Et c'est ainsi pour toute la caisse. Pas de faute d'orthographe, des commentaires pertinents.
J'ai tout mis à la poubelle. On ne pourra plus comparer. C'est ainsi qu'on est le meilleurs. Et tout le monde il est beau et tout le monde il est gentil et tout le monde il est le meilleur. Mais faut pas que les Polonais viennent chez nous piquer nos femmes et nos emplois ! nous allons récrire la Marseillaise.
1998-2008 ! comment en est-on arrivé là ?
Et on nous rebat les oreilles avec ISO 9000.
Pour ma dernière soutenance de stage en sept, un étudiant nous a dit "ce qui a été un peu difficile pour moi, ça a été de me conformer aux normes de spécification de la société qui est de niveau 3 dans le CMI"
Ah ! j'ai vu de quoi il s'agissait. Un tableau où on note :
événements, actions qui s'en suit, éditions éventuelles.
Bientôt un automate de Moore ou de Mealy, ce sera le top du top du top.
Il y a 35 ans nous étions au top niveau sans le savoir.
Il restait une caisse en haut d'une armoire de mon bureau. Comme une échelle était disponible dans le couloir, j'ai finalement pu descendre cette caisse.
Il y avait des classeurs. Je prends le premier en présence d'un collègue qui lui aussi part à la retraite. Je constate qu'il s'agit d'un dossier de td de spec. Le collègue me dit de ne pas l'ouvrir, sinon ça va me mettre le moral à zéro. J'ouvre cependant.
Très bien écrit, bien structuré, enfin un dossier qui respecte les consignes (à une époque où je ne les écrivais pas et où je ne les énonçais qu'une fois dans l'année), un dossier réutilisable, etc. J'avais noté "TB".
De quand date ce dossier ? De 1998.
J'en prends un deuxième. Encore un dossier comme depuis quelques années je n'en vois plus. Et c'est ainsi pour toute la caisse. Pas de faute d'orthographe, des commentaires pertinents.
J'ai tout mis à la poubelle. On ne pourra plus comparer. C'est ainsi qu'on est le meilleurs. Et tout le monde il est beau et tout le monde il est gentil et tout le monde il est le meilleur. Mais faut pas que les Polonais viennent chez nous piquer nos femmes et nos emplois ! nous allons récrire la Marseillaise.
1998-2008 ! comment en est-on arrivé là ?
Et on nous rebat les oreilles avec ISO 9000.
Pour ma dernière soutenance de stage en sept, un étudiant nous a dit "ce qui a été un peu difficile pour moi, ça a été de me conformer aux normes de spécification de la société qui est de niveau 3 dans le CMI"
Ah ! j'ai vu de quoi il s'agissait. Un tableau où on note :
événements, actions qui s'en suit, éditions éventuelles.
Bientôt un automate de Moore ou de Mealy, ce sera le top du top du top.
Il y a 35 ans nous étions au top niveau sans le savoir.
vendredi 5 septembre 2008
Les dossiers de l'an dernier...
sont dans le couloir face au secrétariat.
Pour quelques jours, ensuite poubelle.
Je ne sais si je vais continuer à écrire dans ce bloc-notes. J'envisageai un livre sur le contenu du module spec2. Peut-être ... si les cèpes refusent de sortir par ce mauvais temps.
Pour quelques jours, ensuite poubelle.
Je ne sais si je vais continuer à écrire dans ce bloc-notes. J'envisageai un livre sur le contenu du module spec2. Peut-être ... si les cèpes refusent de sortir par ce mauvais temps.
vendredi 23 mai 2008
La réunion du 22 mai
Elle a duré 1h 45. Il y avait 4 étudiants. Deux excusés. Sur toute une promo. On a pu faire un enseignement de qualité ! et qui plus est en dehors de tout service officiel pour moi. La gratuité ne vaut plus rien a écrit un de mes collègues de Bordeaux. Cette fois elle a eu de la valeur pour quelques étudiants et pour moi.
Je vous avais demandé d'utiliser LTSA pour vérifier...
Dans le corrigé, j'ai fait une erreur de dessin et la réponse à la question 5.3. n'est pas ce qui est imprimé. Certains m'ont écrit comme explication de ce qui n'était pas une erreur (c'est moi qui est fait une erreur !) ..."J'ai répondu ça au lieu de répondre ..." !
En construisant la réponse lors de la réunion, mon erreur a été repérée. Et confirmée
par LTSA. Les outils boîte noire ne sont utiles que pour ceux qui savent ce qu'ils font ! et ce qu'ils en attendent.
Et je ne sais pourquoi j'ai aussi copié des réponses systématiquement fausses pour la question 5.10. Heureusement que des présents à la réunion ont tiqué. Et comme j'ai construit le début d'automate au tableau je me suis aperçu de mon erreur sur le corrigé. J'ai alors demandé aux présents d'utiliser LTSA... et là, on n'a pas obtenu ce que j'attendais !
J'étais bon pour la retraite anticipée ? alors j'ai recommencé sous le contrôle des présents... et ai relu la spec saisie par un étudiant... il n'avait pas saisi la spec de la question (il avait saisi ::, là où dans la spec il y avait :) ! Ouf !
Pour la question 6.3. les présents ne voyaient pas pourquoi il n'y avait pas de solution (impossible de trouver une précondition respectant l'invariant sans modifier ce qui était écrit après le THEN). Et oui ...dans la vie on peut vous poser un pb sans solution. Et il faut savoir repérer. Je vous avais demandé pourquoi.
Comme toujours, impossible de faire faire un diagramme sagittal et un essai illustrant l'impossibilité (il suffit d'exhiber un exemple comme disent les logiciens et c'est démontré !). C'est que nous avons des étudiants qui ne veulent pas s'abaisser à faire des dessins de mat sup (maternelle supérieure). Le prof de maths a vécu cela..; et ça a continué en spec1 et spec2.
Et dès qu'un des 4 présents a eu tenté de faire l'opération sur le diagramme sagittal, il s'est vu comme Archimède ...Eureka.
Alors à vos crayons.
Je vais repasser toutes les copies en revue pour quelques décimales...!
Il est clair que je ne trafiquerai pas les notes. Trafiquer les compteurs sur une automobile est interdit ...
Je vais faire l'ajout des au plus 3 points comme annoncé. Les notes seront donc modifiées conformément aux règles annoncées. Nous vivons dans un état de droit.
Je vous avais demandé d'utiliser LTSA pour vérifier...
Dans le corrigé, j'ai fait une erreur de dessin et la réponse à la question 5.3. n'est pas ce qui est imprimé. Certains m'ont écrit comme explication de ce qui n'était pas une erreur (c'est moi qui est fait une erreur !) ..."J'ai répondu ça au lieu de répondre ..." !
En construisant la réponse lors de la réunion, mon erreur a été repérée. Et confirmée
par LTSA. Les outils boîte noire ne sont utiles que pour ceux qui savent ce qu'ils font ! et ce qu'ils en attendent.
Et je ne sais pourquoi j'ai aussi copié des réponses systématiquement fausses pour la question 5.10. Heureusement que des présents à la réunion ont tiqué. Et comme j'ai construit le début d'automate au tableau je me suis aperçu de mon erreur sur le corrigé. J'ai alors demandé aux présents d'utiliser LTSA... et là, on n'a pas obtenu ce que j'attendais !
J'étais bon pour la retraite anticipée ? alors j'ai recommencé sous le contrôle des présents... et ai relu la spec saisie par un étudiant... il n'avait pas saisi la spec de la question (il avait saisi ::, là où dans la spec il y avait :) ! Ouf !
Pour la question 6.3. les présents ne voyaient pas pourquoi il n'y avait pas de solution (impossible de trouver une précondition respectant l'invariant sans modifier ce qui était écrit après le THEN). Et oui ...dans la vie on peut vous poser un pb sans solution. Et il faut savoir repérer. Je vous avais demandé pourquoi.
Comme toujours, impossible de faire faire un diagramme sagittal et un essai illustrant l'impossibilité (il suffit d'exhiber un exemple comme disent les logiciens et c'est démontré !). C'est que nous avons des étudiants qui ne veulent pas s'abaisser à faire des dessins de mat sup (maternelle supérieure). Le prof de maths a vécu cela..; et ça a continué en spec1 et spec2.
Et dès qu'un des 4 présents a eu tenté de faire l'opération sur le diagramme sagittal, il s'est vu comme Archimède ...Eureka.
Alors à vos crayons.
Je vais repasser toutes les copies en revue pour quelques décimales...!
Il est clair que je ne trafiquerai pas les notes. Trafiquer les compteurs sur une automobile est interdit ...
Je vais faire l'ajout des au plus 3 points comme annoncé. Les notes seront donc modifiées conformément aux règles annoncées. Nous vivons dans un état de droit.
vendredi 16 mai 2008
Détails
"Mais ce n'est pas assez que d'avoir bien établi l'ensemble, il s'agit d'y introduire les détails sans détruire la masse."
Diderot, Essais sur la peinture, Hermann, page 17 *
En informatique, nous disposons des techniques d'abstraction, de raffinage. C'est ce que nous avons tenté d'enseigner en spec1 et spec2.
* merci à Sébastien qui m'alimente en ouvrages
Diderot, Essais sur la peinture, Hermann, page 17 *
En informatique, nous disposons des techniques d'abstraction, de raffinage. C'est ce que nous avons tenté d'enseigner en spec1 et spec2.
* merci à Sébastien qui m'alimente en ouvrages
Inscription à :
Articles (Atom)
