JFLA 2023 : Références au développement Coq

Cette page présente le développement Coq associé à l'article "Analyse de dépendance vérifiée pour un langage synchrone à flot de données" de T. Bourke, B. Pesin et M. Pouzet, soumis aux JFLA 2023. Les liens suivants permettent de retrouver les définitions formelles Coq présentées dans les différentes parties de l'article.

1 Introduction

Nous proposons une démonstration en ligne du compilateur et d'un interpréteur pour le langage Vélus. Le programme est extrait de Coq et compilé en Javascript par js_of_ocaml. Il est accompagné d'un simulateur permettant de tester l'exemple présenté dans l'article.

2 Sémantique à flots de donnés de Vélus

• LSyntax: Syntaxe abstraite de Lustre
• exp: expressions
• block: blocs
• node: noeuds
• global: programmes

2.1 Noyau du langage

• LSemantics: Règles sémantiques pour Lustre
• Svar: Sémantique d'une variable
• Sconst: Sémantique d'une constante
• const: Flot constant échantillonné
• sem_equation: Sémantique d'une équation
• sem_node: Sémantique d'un noeud
• fby: opérateur co-inductif pour le fby
• fby1: opérateur co-inductif auxiliaire pour le fby
• Sfby: Sémantique du fby

2.2 Structure de contrôle switch

• when: opérateur co-inductif pour le when
• when_hist: when appliqué à un historique
• Sswitch: Sémantique d'un switch

2.3 Déclarations locales

• union: opérateur d'union d'historiques
• Sscope: Sémantique d'une déclaration locale
• Slast: Sémantique de l'expression last

3.1.1 Variables utilisées instantanément

• Is_free_left: Variables utilisée instantanément dans une expression
• Is_free_left_list: Variables utilisée instantanément dans une liste d'expressions

3.1.2 Variables définies et dépendances

• DefEq: Etiquettes définies par une équation
• DepOnEq: Dépendances induites par une équation
• DefScope: Etiquettes définies par une déclaration locale
• DepOnScope1: Dépendances des sous-blocs d'une déclaration locale
• DepOnScope2: Dépendances des déclarations last
• DefBranch1: Etiquettes définie par les sous-blocs d'un switch
• DepOnBranch1: Dépendances des sous-blocs d'un switch
• DefBranch2: Etiquettes renommée par les substitutions d'un switch
• DepOnSwitch2: Dépendances de contrôle d'un switch
• DepOnBranch2: Dépendances induites par les substitutions d'étiquettes d'un switch

3.2 Analyse du graphe de dépendance

• AcyGraph: formalisation d'un graphe acyclique
• dfs: fonction de recherche en profondeur dans un graphe
• node_causal: définition d'un noeud "causal"

4.1 Principe d'induction sur les étiquettes

• TopoOrder: ordre topologique sur les étiquettes
• has_TopoOrder: existence d'un ordre topologique
• node_causal_ind: principe d'induction sur les étiquettes

4.2 Principe d'induction sur les expressions

• exp_causal_ind: principe d'induction sur les expressions

4.3 Application: déterminisme de la sémantique

• det_global: déterminisme de la sémantique
• EqStN: équivalence jusqu'à n
• det_exp_S: équivalence jusqu'à n + 1 pour les expressions
• fby_det_Sn: équivalence jusqu'à n + 1 pour fby
• sem_scope_det: sémantique instrumentée, cas de la déclaration locale
• det_block_S: Sémantique instrumentée, passage de n à n + 1