Proof of correctness of the Mazoyer's solution of the firing squad problem in Coq
In: https://hal-lara.archives-ouvertes.fr/hal-02101837 ; [Research Report] LIP RR-2002-14, Laboratoire de l'informatique du parallélisme. 2002, 2+36p, 2002
Online
report
Zugriff:
The firing squad synchronization is a cellular automata problem introduced by Moore; in 1987, J.Mazoyer gave a six state solution to this problem. The proof of correctness of this solution uses discrete geometrical considerations, but is quite hard to verify due to the multiplication of cases and indexes. To be more confident in this proof, a proof assistant developed by the Inria, Coq has been used. This report exposes the development in Coq of this proof. A large use of inductive structures, a natural way in Coq, offers a clearer vision of the Mazoyer's solution. The full development of the proof is avalaible in the contributions of the Coq software. ; La synchronisation d’une ligne de fusiliers est un problème d’automates cellulaires posé par Moore, en 1987, J.Mazoyer donna une solution avec six états à ce problème. La preuve de correction de cette solution utilise des considérations de géométrie discrète, mais elle est assez difficile à vérifier à cause de la multiplication des cas et des indices. Pour être plus sûr de cette preuve, un assistant à la preuve développé par l’Inria, Coq, a été utilisé. Ce rapport expose le développement en Coq de la preuve. Un grand usage des structures inductives, une voie naturelle en Coq, offre une vision plus claire de la solution de J.Mazoyer. Le développement complet de la preuve est disponible dans les contributions du logiciel Coq
Titel: |
Proof of correctness of the Mazoyer's solution of the firing squad problem in Coq
|
---|---|
Autor/in / Beteiligte Person: | Duprat, Jean ; Laboratoire de l'Informatique du Parallélisme (LIP) ; École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL) ; Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS) ; Laboratoire de l'informatique du parallélisme |
Link: | |
Zeitschrift: | https://hal-lara.archives-ouvertes.fr/hal-02101837 ; [Research Report] LIP RR-2002-14, Laboratoire de l'informatique du parallélisme. 2002, 2+36p, 2002 |
Veröffentlichung: | HAL CCSD, 2002 |
Medientyp: | report |
Schlagwort: |
|
Sonstiges: |
|