Hello!

Inspiré(e) de prendre part à la discussion ? Ou de poser une question ou demander de l’aide ?

Alors bienvenues dans les grands sujets des forums de La Bulle : m’inscrire.

Cette partie du forum n’est pas compatible avec les bloqueurs publicitaires

Félicitations à vous, de préférer les accès payants plutôt que la gratuité par la publicité, c’est honnorable et cohérent de votre part. Malheureusement, l’accès payant par micropaiement (qui serait d’environ 1 cent pour 20 pages consultées) n’est pour l’instant pas encore mis en place, et l’accès gratuit sans publicité, est réservé aux membres actif(ve)s du forum. En attendant, si vous souhaitez poursuivre votre visite chez nous, vous pouvez ajouter le site à votre liste blanche, ou encore mieux, désactiver le bloqueur partout. Pour ajouter le site à votre liste blanche, pour Firefox (similaire pour les autres navigateurs), rendez‑vous en bas à gauche de la fenêtre de votre navigateur, et cliquez sur le menu comme dans l’exemple de l’image ci‑dessous, puis rechargez la page, en appuyant sur F5.

Programming from Specifications, par Carroll Morgan (1990‑1998)
Auteur Message
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17338
Dim 19 Fév 2012 21:36
Message 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 :
Carroll Morgan a écrit : 
© Carroll Morgan 1990, 1994 and 1998.

Permission is granted to copy this material for private study; for other uses please contact the author.

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.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17338
Mar 28 Fév 2012 22:10
Message Re: Programming from Specifications, par Carroll Morgan (1990‑1998)
J’ajoute quelques liens en vrac sur le même thème.


(*) 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.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17338
Mar 28 Fév 2012 22:25
Message Re: Programming from Specifications, par Carroll Morgan (1990‑1998)
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.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17338
Jeu 23 Mai 2013 14:44
Message Re: Programming from Specifications, par Carroll Morgan (1990‑1998)
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 :
Les auteurs a écrit : 
This electronic book is a one-semester course on Software Foundations — the mathematical theory of programming and programming languages


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.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17338
Ven 23 Aoû 2013 22:02
Message Re: Programming from Specifications, par Carroll Morgan (1990‑1998)
Voir aussi le sujet : « Sites sur l’analyse structurée dans le logiciel ».

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17338
Lun 18 Nov 2013 17:23
Message Re: Programming from Specifications, par Carroll Morgan (1990‑1998)
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.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17338
Sam 28 Déc 2013 13:48
Message Re: Programming from Specifications, par Carroll Morgan (1990‑1998)
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.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17338
Dim 6 Avr 2014 15:37
Message Re: Programming from Specifications, par Carroll Morgan (1990‑1998)
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 Clin d’œil .

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.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17338
Jeu 17 Avr 2014 05:00
Message Re: Programming from Specifications, par Carroll Morgan (1990‑1998)
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.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17338
Mar 23 Sep 2014 04:51
Message Re: Programming from Specifications, par Carroll Morgan (1990‑1998)
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é :
Roger Bishop Jones a écrit : 
I rather liked using functional programming languages for writing small "formal" specifications of various things to do with languages (abstract syntax, deductive systems).

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet