Page d'accueil

Ces pages font l'objet d'une (re)construction permanente.

Actualitės

Lothar Collatz (en 1937) avait raison.

La carte

Sur ces pages, nous présentons quatre projets de recherche: Algorithmic Logic (ou calcul des programmes) (depuis 1968), Loglan'82 (de 1978), SpecVer(2007), Lem (2012). Les deux premiers projets ont donné de nombreux résultats et seront utilisés pendant de nombreuses années.

Le projet de rechercheLa logique algorithmiquepour découvrir des loisle compte de programmeet est applicable dans la vérification des programmes, c'est-à-dire dans la preuve de l'exactitude de la propriété des programmes tels queL'exactitude, n'étant pas invivable et d'autres. Le langage de la logique algorithmique permet non seulement d'exprimer les propriétés des algorithmes (programmes), mais aussi d'apxiomatiquer de nombreuses structures de données. Les deux sont bien connus et nécessaires dans les algorithmes, par exemple les piles, les arbres de recherche, les monticules, etc., ainsi que de nombreuses structures étudiées en mathématiques. On peut considérer que les mathématiques sont engagées dans l'étude de la question de savoir si une formuleLes et ' C'est vrai dans la structureA et A et . . Mais la plupart des structures ne peuvent pas être décrites avec des axiomes écrits dans la langue du premier ordre. L'adoption du langage de la logique algorithmique (sauf le langage algorithmique) vous permet de fournir...

La logique algorithmique - Algorithmique Notice logique Le projet de rechercheLoglan'82Il a apporté un langage de programmation orienté objet et distribué du même nom. La publication de la langue et la distribution du compilateur ont été précédées de questions de recherche. Mentionnons par exemple:

Résoudre le problème de la désallocation sûre et efficace d'objets inutiles. La solution au problème (statique) de la sémantique qui se produit lorsque les modules de classe peuvent être imbriqués (classes intérieures) et élargis (inheritation). Le protocole original de coopération des objets de processus que le programmeur peut allouer dans un réseau informatique ( protocole d'appel extraterrestre). Loglan a été créé de nombreuses années avant C'(1986) et Java (1995). Ces deux (et autres) langages de programmation n'ont pas appris les solutions connues dans Loglan depuis plus de 30 ans. En savoir plus sur Loglan peut changer complètement votre vision de l'ingénierie logicielle. En localisant les connaissances et les compétences offertes par Loglan, vous pouvez améliorer considérablement vos qualifications. Loglan'82 La brochure Loglan'82 LEM est le nom d'un nouveau projet de recherche.

L'objectif de ce projet est d'étudier si un langage de programmation présentant certaines caractéristiques spécifiques peut être créé (voir spécification LEM). Le langage LEM est de s'appuyer sur les réalisations du projet Loglan'82 et d'utiliser ce qui est bon dans les langages de programmation de terrain des nouvelles générations: Java, C, C, python, etc. MALME Le projet SpecVer vise à confirmer l'utilité d'appliquer les lois de la logique algorithmique en ingénierie logicielle. LME peut être utile dans le travail de SpecVer.

SpecVer Une bibliothèque de classes et de connaissances mathématiques utiles aux programmeurs.

Vision de l'avenir (un projet de plus pour de nombreuses années de travail).

Commençons par quelques questions : est-il possible d'inclure des connaissances mathématiques dans votre ordinateur ? Est-il possible d'inclure les connaissances informatiques dans l'ordinateur? D. D. Knuth avait une telle ambition dans les années 1970, en commençant sa création de son Art of Programming. Aujourd'hui, aprè

ement, les ordinateurs sont beaucoup plus grands et beaucoup plus rapides qu'ils ne l'étaient, deuxièmement, il y a un réseau informatique. (La vision de S est réalisée. Lema des années 1950). Cela nous permet de passer à l'esquisse du concept: Ce serait :

   Créer une réserve de connaissances utilisées par les développeurs de logiciels. Il y aura des bibliothèques de classes et de méthodes et de connaissances sur les structures de données dans lesquelles les calculs sont effectués. Cela s'applique à la fois aux structures relationnelles (algébriques) considérées par les mathématiciens et aux structures des données définies et utilisées par les ingénieurs logiciels.
   Créer un langage dans lequel les développeurs de logiciels écriront leurs arguments en faveur des messages faits (imprimés, distribués, ...), une telle langue devrait être lisible pour les personnes et suffisamment formalisée pour être possible à l'analyse informatique des preuves présentées.
   un outil permettant de vérifier l'exactitude des preuves. Vous aurez besoin d'un vérificateur de preuve, mais significativement différent de Mizar et d'autres similaires, parce que les preuves seront sauvegardées dans le compte du programme (c'est-à-dire le système AL) plus riche que le compte prédicat,
   Pensez à la façon dont les connaissances sont collectées et partagées. Est-ce une sorte de moteur de recherche Google pour l'algorithme mathématique ?

Les questions