Notation mathématique des concepts de programmation
https://stackoverflow.com/questions/1632786
-
06-07-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
RussianQuestion
Il existe de nombreuses méthodes pour représenter la structure d'un programme (comme les diagrammes de classes UML, etc.). Je suis intéressé s’il existe une convention décrivant les programmes de manière stricte et mathématique. Je suis particulièrement intéressé par l'utilisation de la notation mathématique à cette fin.
Un exemple : les classes sont représentées sous la forme d'ensembles (champs, propriétés) et de fonctions (opérant sur les éléments des ensembles). Les champs d'une classe parente sont un sous-ensemble de la classe enfant. Les fonctions sont décrites dans un pseudocode qui doit ressembler à ceci et cela ...
La solution
Je sais que la notation Z a été utilisée dans une certaine mesure dans la vérification formelle de logiciels, telle que le projet Tokeneer .
Autres conseils
Oui, il existe Floyd Logique des caisses .
Il y a beaucoup de chemin, mais je pense que la plupart d’entre eux sont peu pratiques pour exprimer la structure car celle-ci n’est souvent pas exprimable dans des concepts mathématiques par défaut. La principale exception concerne bien entendu les langages de programmation fonctionnels. Pensez aux plis (catamorphisme), aux groupes, à l’algèbre, etc.
Pour la programmation impérative, je connais l’existence de Z, qui utilise la théorie des ensembles de calcul lambda (pur et étendu) et la logique des prédicats (du premier ordre). Cependant, je ne pense pas que ce soit très pratique. Le seul avantage de l’utilisation des mathématiques pour exprimer une structure est le fait que vous pouvez prouver quelque chose à ce sujet. Mais si vous voulez faire cela, jetez un coup d’œil à JML, Spec # ou Eiffel.
Cela dépend de ce que vous essayez d'accomplir, mais le fait de choisir des langues spécifiques peut vous causer des ennuis.
Par exemple, consultez la discussion cercle-ellipse . FAQ C ++ Lite.
Ce livre applique la méthode déductive à la programmation en affiliant des programmes avec la mathématique abstraite théories qui leur permettent de travailler. [...]
Je pense que les Eléments de programmation d'Alexander Stepanov et de Paul McJones sont assez proches de ce que vous êtes. à la recherche de.
Un concept est une description de exigences sur un ou plusieurs types déclaré en termes de l'existence et propriétés des procédures, type attributs et fonctions de type définis sur les types.
Z, qui a déjà été mentionné, est à peu près ce que vous décrivez. Il en existe quelques variantes pour la modélisation orientée objet, mais je pense que vous pouvez aller assez loin avec & "Standard Z's &"; schémas si vous souhaitez modéliser des classes.
Il existe également Alloy , une version plus récente inspirée de Z. Sa notation est peut-être un peu plus proche de l'objet. -orientation. Il est également analysable, c’est-à-dire que vous pouvez vérifier si les modèles que vous créez remplissent certaines conditions, mais il ne peut pas prouver que les propriétés sont valables. Vous devez simplement essayer de les réfuter dans un périmètre fini.
L'article Un logiciel fiable par conception est une belle introduction à Alloy. et son genre, avec un tableau des outils similaires disponibles.
Vous recherchez une programmation fonctionnelle. Il existe plusieurs langages de programmation fonctionnels, et ils sont Le tout basé sur une théorie mathématique fondamentale appelée Calcul Lambda . Les programmes écrits dans un langage de programmation fonctionnel tel que LISP sont une représentation mathématique d'eux-mêmes. ; -)
Il existe un langage mathématique qui décrit en fait un programme ou plutôt ses opérations. Vous prenez l'état initial puis transformez cet état jusqu'à atteindre l'état cible souhaité. Les transformations donnent le code du programme qui doit être exécuté.
Consultez l'article sur la logique de Hoare dans Wikipedia.
L'idée de base est que pour chaque fonction (que vous l'insériez dans une classe ou dans une fonction de style ancien), vous avez une condition préalable et une condition ultérieure. Par exemple, la condition préalable peut être que vous ayez un tableau comportant >= 0 éléments. la post-condition est que chaque élément [i] doit être par < = élément [j] pour chaque i < = j.
La description habituelle serait & "; la fonction trie le tableau &"; Mais les termes mathématiques vous permettent de transformer l’entrée (qui doit correspondre à la condition préalable) en une sortie (qui doit correspondre à la condition suivante).
Il est un peu difficile à utiliser, en particulier pour les programmes plus complexes, mais certains exemples sont assez impressionnants. Le résultat est souvent un code très compact, ce qui peut paraître complexe, mais fonctionne au premier essai.
J'aimerais suggérer une algèbre de la programmation . Il s’agit d’une approche calculatrice des programmes, qui utilise Algèbre relationnelle et Connexions Galois .
Si ce sujet vous intéresse, vous pouvez trouver un article étonnant, ici , par Shin-Cheng Mu, et Jos & # 233; Nuno Oliveira ( diapositives ).
L’utilisation de l’algèbre relationnelle et de la logique du premier ordre offre également une belle synergie avec Alliage , la programmation fonctionnelle et Conception par contrat (facilement applicable à la programmation orientée objet).
