Une méthode de raffinement et de développement pour la programmation parallèle : econtribution à l'étude du raffinement de programmes parallèles : une approche fondée sur le concept de preuve - Université de Lorraine Accéder directement au contenu
Thèse Année : 1993

A method for refining and developing concurrent programs : on the study of refinement of concurrent programs : ea proof-based approach

Une méthode de raffinement et de développement pour la programmation parallèle : econtribution à l'étude du raffinement de programmes parallèles : une approche fondée sur le concept de preuve

Dominique Méry

Résumé

Not available
Ce document présente l'étude de la relation entre la preuve de programmes parallèles et le raffinement de spécifications formelles en programmes parallèles (ou communicants). Il vise à intégrer les systèmes axiomatiques de preuve dans la démarche de construction pas-à-pas de programmes parallèles à partir de spécifications formelles, telles que les propriétés d'invariance et de fatalité. Nous avons dégagé des transformations relatives à des classes de programmes (parallèles) à partir d'études de cas. La relation de raffinement est fondée sur la préservation des propriétés déjà acquises ou démontrées. Elle admet une sémantique exprimée à l'aide des transformateurs de prédicats spécifiques à la classe considérée mais elle admet une autre sémantique fondée sur le système formel lui-même et sur la notion de preuve. Les transformations sont correctes par rapport à ces deux sémantiques équivalentes. La thèse de ce document peut se résumer comme suit: raffiner un programme en un autre programme suivant une sémantique de transformation de prédicats revient à raffiner la spécification du programme selon les règles du système formel construit à l'aide des transformateurs de prédicats. La structuration des informations à manipuler a conduit à proposer un langage pour les termes de développement comprenant, pour chaque terme, la spécification, la documentation formelle, le programme et l'environnement. Le lieu entre les différents termes est défini par la relation de raffinement (en accord avec les transformateurs de prédicats ou en accord avec les règles)
Fichier non déposé

Dates et versions

tel-01753615 , version 1 (29-03-2018)

Identifiants

  • HAL Id : tel-01753615 , version 1

Accès intranet

Citer

Dominique Méry. Une méthode de raffinement et de développement pour la programmation parallèle : econtribution à l'étude du raffinement de programmes parallèles : une approche fondée sur le concept de preuve. Autre. Université Henri Poincaré - Nancy 1, 1993. Français. ⟨NNT : 1993NAN10019⟩. ⟨tel-01753615⟩
54 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More