Quelqu'un a-t-il déjà écrit un système (logiciel ou explication détaillée sur papier avec des exemples simples) qui génère des programmes informatiques? J'entre et il crée un programme qui répertorie les nombres premiers inférieurs à 10. P r i m e ( x ) est simplement défini comme 1 < x ∧ ∄ A professeurs disent qu'ils le peuvent mais personne ne donne d'exemples complets réels.
17
Réponses:
Il s'agit d'un sujet de recherche très actif, très prometteur, bien que l'automatisation complète de la génération de programmes ait probablement des limites intrinsèques (mais les êtres humains sont-ils meilleurs?). Mais l'idée est toujours très utile pour aider considérablement à la création de programmes en mécanisant de nombreuses étapes, et en vérifiant automatiquement l'exactitude de la génération du programme.
Elle est fortement liée à un résultat en logique, appelé la correspondance de Curry-Howard (ou isomorphisme), qui montre que les programmes informatiques et les preuves mathématiques sont très similaires.
L'idée est donc que le système prendra votre spécification de programme comme un théorème à prouver. Dans le cas de votre exemple, ce serait quelque chose comme (officieusement): "il y a un ensemble de tous les nombres premiers inférieurs à 10".
Ensuite, vous tenterez de prouver ce théorème, et les systèmes existants vous aideront à faire la preuve, à automatiser certaines parties, éventuellement la preuve entière, et à vous assurer de ne jamais faire d'erreurs.
De cette preuve, on peut ensuite extraire un programme qui calcule réellement la liste souhaitée des nombres premiers qui avaient été initialement spécifiés.
Plusieurs systèmes ont été développés dans le passé pour élucider ces idées. L'un des plus connus était LCF de Robin Milner , qui a créé le langage ML à cet effet. L'un des systèmes actuellement les plus avancés est Coq .
Il existe des exemples entièrement élaborés, certains assez complexes. Vous pouvez en trouver dans l' article suivant , bien qu'il ne s'agisse en aucun cas d'une lecture simple et nécessite des connaissances avancées de Logic.
la source
La réponse wag: Oui, mais au moment de la rédaction, pour la plupart des programmes non triviaux, les spécifications semblent être aussi difficiles à écrire et à déboguer que les programmes.
Plus sérieusement, la réponse de babou est bonne, mais je vais également suggérer de vérifier la zone des types dépendants. Il y a un assez bon livre utilisant Coq (avertissement complet: écrit par un de mes amis), mais il y a aussi Epigram, Agda et Idris. Isabelle / HOL vaut également le détour.
Tout cela est basé sur le calcul des constructions. Si vous voulez connaître la base théorique, recherchez la théorie des types de Martin-Löf. Il y a d'excellentes présentations.
la source
Commençant ici dans une tangente, les générateurs de programmes (c'est-à-dire les systèmes qui ont donné une description de haut niveau de quelque chose dans un langage spécial) existent depuis toujours. Tout compilateur en fait partie, tout comme l'un des nombreux générateurs d'analyseurs. À l'époque, les systèmes appelés «langues de troisième génération», qui généraient (la plupart du) le code d'une application métier typique, étant donné une description de haut niveau et un catalogue de données disponibles, étaient populaires.
la source
La programmation logique et, plus généralement, la programmation déclarative prennent comme prémisse exactement ce que vous proposez: à savoir, à partir d'une spécification logique, renvoyer un résultat satisfaisant à cette spécification.
Un domaine qui semble répondre spécifiquement à l'exemple des "nombres premiers inférieurs à 10" que vous donnez est la programmation par contraintes qui essaie de trouver des solutions aux problèmes impliquant certaines contraintes, y compris des contraintes entières comme celles que vous avez données.
Vous voudrez peut-être essayer ECLiPSe pour une implémentation spécifique (open source) d'un tel système.
la source