Programming from Specifications, par Carroll Morgan (1990‑1998)

Un magnifique livre en ligne dont quelqu’un vient de me donner le lien sur un Usenet.

Ça s’adresse aux gens qui on horreur du bricolage quand on leur parle de conception logicielle, et aime faire des preuves de fonctionnement (autant que possible, parce qu’il est difficile d’appliquer des méthodes formelles partout).

http://www.cs.ox.ac.uk/publications/books/PfS/

Les chapitres sont tous au format PostScript. Les utilisateurs de Windows auront peut‑être des difficultés pour les ouvrir, le PostScript ne pouvant y être ouvert nativement.

Si vous ne voulez pas avoir un fichier par chapitre, mais avoir le tout en un seul fichier, passez par le lien en bas de page, ou directement : PfS.ps.gz. 500KB.

Conditions d’utilisation :

En résumé, la redistribution est interdite. Si vous souhaitez faire connaitre cet eBook, vous ne pouvez le faire que en donnant les liens ci‑dessus. Les copies que vous en faites doivent être réservées à un usage strictement d’études personnelles. Vous ne pouvez pas mettre cet eBook en téléchargement sur votre propre site. Vous ne pouvez pas en copier le contenu sur un site (sauf de courtes citations, et sans oublier de les attribuer à l’auteur).

Le lien de contact, si il est nécessaire, est donné en haut de page du premier lien.

J’ajoute quelques liens en vrac sur le même thème.

• Logic in Coq (seas.upenn.edu). 22 Février 2012.
• Type Theory (plato.stanford.edu). Février 2006 ‑ Janvier 2010.
• The Development of Proof Theory (plato.stanford.edu). Avril 2008.
• Intuitionism in the Philosophy of Mathematics (plato.stanford.edu). Septembre 2008.
• Constructive Mathematics (plato.stanford.edu). Mai 2009.
• Software Foundations (cis.upenn.edu). Octobre 2011.
• Coq'Art Home page (labri.fr) (*). Date inconnue.

(*) Version en ligne d’un livre initialement publié en version papier.

D’autres liens à venir sur ce sujet complexe mais passionnant tout autant que fondamentalement utile.

Un autre

Formalizing 100 Theorems (cs.ru.nl)

C’est une collection de théorèmes démontrés avec des assistants de preuves formelles, dont Coq, Isabelle et PVS.

Dans le même domaine de la conception logicielle, des méthodes formelles, et des fondement théoriques (cependant pour la pratique !) de l’informatique, un autre livre consultable en ligne. Une version téléchargeable pour une consultation hors‑ligne est également proposée.

La première phrase d’introduction du livre en guise de description :


Voir : Software Foundations (cis.upenn.edu)

Par

• Benjamin C. Pierce
• Chris Casinghino
• Michael Greenberg
• Cătălin Hriţcu
• Vilhelm Sjöberg
• Brent Yorgey

Remarque : les preuves formelles décrites dans ce livre, sont toutes écrites dans le langage de l’assistant de preuves Coq; il ne couvre pas Isabelle/HOL.

Une chose amusante, est la manière dont est présentée la structure du livre en guise d’aperçu : avec un schéma digne d’un diagramme d’analyse, et qui indique le parcours de lecture à la manière des cookbooks que l’on peut trouver dans la documentation des sources de quelques rares logiciels.

Voir sur la page : Overview

Je ne l’ai pas encore lu, je ferai peut‑être d’autres commentaires quand ce sera fait.

Voir aussi le sujet : « Sites sur l’analyse structurée dans le logiciel ».

En rapport, parce qu’il a été question ici de HOL et parce qu’il s’agit de preuves sur des programmes, un lien vers un article expliquant les différences entre la théorie des ensembles et la théorie des types.

Type theory versus set theory (planetmath.org).

Cette page est un chapitre de PMBookProject (planetmath.org), PM, signifiant Planet Math.

Je disais plus haut que la question de la théorie des types vs la théorie des ensembles, méritait un lien ici : c’est parce que la notion de type est autant essentielle aux programmes que la notion de fonction, et également parce que les notions de logique d’ordre supérieur (HOL = Higher Order Logic) et de théorie des types, sont intimement liées.

Moins strictement formalisé, le classique de Alfred Aho and Jeffrey Ullman, peut être mentionné ici quand‑même : Foundations of Computer Science (stanford.edu). Le livre qui n’est plus disponible en version papier, peut y être obtenu au format PDF ; un par chapitre.

Assez directement relié aux preuves des programmes, est la formalisation des mathématiques, formalisations écrites dans un langage permettant la validation mécanique des preuves.

J’ai pensé poster ces liens dans le sujet sur notes en vrac sur la logique, mais comme c’est plus à propos des applications de la logique qu’à propos des logiques elles‑mêmes, c’est posté ici.

Le premier lien, est une page renvoyant elle‑même vers d’autres sites. Je ferai peut‑être un trie plus tard, parmi les liens qu’elle propose.

What is Formal Math? (vdash.org) : une liste de liens sur les langages et résultats existant dans la formalisation des mathématique. La page d’accueil, www.vdash.org, trahis une préférence de l’auteur pour le langage Isabelle/Isar .

WikiProofs.org : un wiki dédié aux preuves de théorèmes mathématiques. Les preuves sont validées par le système JHilbert (mediawiki.org), une extension de MédiaWiki, comme l’explique le tutoriel de WikiProof. J’ai découvert ce wiki à travers sa présentation dans une page blog spécialisé dans l’actualité et les pensées sur la formalisation des mathématique, The first formalized math wiki is here (slawekk.wordpress.com).

Formalized Mathematics (slawekk.wordpress.com) : le blog qui informant de l’existence wiki présenté ci‑dessus.

Metamath (us.metamath.org) : un des langages de formalisation des mathématiques, vers lequel lie le premier site introduit dans ce message.

Une présentation au format PDF, comme introduction au DbC (Design by Contract ™) avec la logique de Hoare.

Rigorous Software Engineering — Hoare Logic and Design by Contracts (di.ubi.pt) [PDF]. Simão Melo de Sousa. 2011. Université de Beira Interior, Portugal.

www.rbjones.com/rbjpub/rbjcv/docarch/

La page n’a aucun titre. Elle est à propos Z et VDM (Vienna Development Method).

Une chose notable, est que cette page liste des spécifications en SML [1]. C’est par un de ces documents, celui spécifiant la syntaxe abstraite de VDM en SML, que j’ai découvert cette page : The abstract syntax of VDM in SML [PDF]. Ce n’est pas le seul, il y en a d’autres.

[1]: L’auteur mentionne explicitement cette spécificité :