Résumé:
L'aléatoire est introduit sous la forme d'une simple instruction
d'affectation
Nous montrons comment étendre le système d'inférence de la Sémantique Axiomatique (SA) de Hoare par l'ajout d'une seule régle, spécifique à cette nouvelle instruction. Le cadre étudié fait apparaître quelques particularités sur le plan logique : caractère « intuitionniste », relation entre terminaison et convergence de série.
Ce travail s'appuie sur une proposition de sémantique dénotationnelle proposée par Dexter Kozen (1981) et un résultat plus général montrant comment il est possible de reconstruire les règles de la SA en correction partielle à partir d'une sémantique par continuations du langage étudié. Comme conséquence immédiate, blocs d'instructions étiquetées et exceptions n'offrent aucune difficulté supplémentaire.
L'exposé sera accompagné de quelques exemples simples de calculs.
See this web page for more information.
Retour au sommaire / Back to schedule