Sémantique formelle d'OCaml dans Coq

14

La sémantique d'un grand sous-ensemble d'OCaml, appelé OCamllight , a été formalisée dans HOL par Owens il y a plusieurs années. Plus récemment, une sémantique théorique de type d'un plus petit sous-ensemble d'OCaml a été implémentée dans Nuprl par Kreitz, Hayden et Hickey .

Y a-t-il un développement similaire à Coq?

coq program-verification ocaml Andrea Asperti
la source
Vous pourriez être intéressé par CakeML: cakeml.org . Ce n'est pas spécifiquement OCaml, cependant.
jmite

Réponses:

12

Avez-vous vu la thèse d'Arthur Charguéraud, Formules caractéristiques pour la vérification de programme mécanisée ?

Plutôt que de construire le système de types et la sémantique à petits pas comme des relations inductives, il donne une technique pour convertir les programmes Caml en formules caractéristiques. Il s'agit essentiellement d'une généralisation de la sémantique des transformateurs de prédicats pour prendre en charge un très grand sous-ensemble d'Ocaml - notamment, y compris les transtypages non sécurisés comme Obj.magic. Pour citer sa thèse:

Je me suis concentré sur un sous-ensemble du langage de programmation OCaml, qui est un langage de programmation de haut niveau séquentiel, appelé par valeur. L'implémentation actuelle de CFML prend en charge le λ-calcul de base, y compris les fonctions d'ordre supérieur, la récursivité, la récursion mutuelle et la récursivité polymorphe. Il prend en charge les tuples, les constructeurs de données, la correspondance de modèles, les cellules de référence, les enregistrements et les tableaux. Je fournis une bibliothèque Caml supplémentaire qui ajoute la prise en charge des pointeurs nuls et des mises à jour solides.

C'est une approche très attrayante si vous voulez prouver qu'un programme Caml particulier est correct (moins si vous êtes intéressé par sa métathéorie, cependant).

Neel Krishnaswami
la source
Donc, si je comprends bien, la spécification de la sémantique d'Ocaml est intégrée dans le système. Est-il possible d'interpréter la formule caractéristique de (une fonction clé du) système comme une telle spécification? De plus, je suppose que le système est écrit en OCaml. Est-il possible de spécifier et de prouver son exactitude dans le système lui-même?
Andrea Asperti
Pour un programme OCaml donné, sa formule caractéristique peut être considérée comme une sémantique dénotationnelle, une spécification "la moins générale" qui peut être utilisée pour prouver toutes les propriétés souhaitables du programme. Si vous parlez de la «justesse» du CFML lui-même, la question est: par rapport à quelle sémantique formelle alternative?
gasche
Étrange d'avoir un programme qui est censé certifier un logiciel et dont le comportement ne peut être spécifié :)
Andrea Asperti
@AndreaAsperti Qu'entendez-vous par "intégré dans le système"? L'idée derrière les formules caractéristiques (CF) est assez simple: mapper les programmes sur des formules logiques (généralement pré- et postcondition) telles que les formules décrivent précisément la sémantique des programmes. En d'autres termes, deux programmes satisfont les mêmes FC si ils ne peuvent être différenciés contextuellement. La cartographie du programme vers les CF se fait par induction de la structure du programme, et peut cibler toute logique suffisamment expressive. A. Charguéraud cible la logique de Coq, mais c'est un choix contingent.
Martin Berger
1
@MartinBerger: le papier de Guéneau et al prouve seulement la solidité parce que les pré / posts dérivés ne caractérisent pas les programmes dont ils dérivent. Leurs CF dérivent de la sémantique non typée de CakeML, mais le langage typé a une équivalence d'observation différente. (Pour une vérification pratique, ce n'est pas très important et c'est plus facile.)
Neel Krishnaswami
8

Vous pourriez être intéressé par Une implémentation certifiée de ML avec type de polymorphisme structurel et types récursifs de Jacques Garrigue , qui établit la solidité de la sémantique statique et dynamique et les propriétés d'inférence de type pour un langage ML avec ( polymorphisme récursif et) structurel, formalisant ainsi l'un des coins plus avancés d'OCaml (variantes polymorphes et types d'objets).

Cela dit, ce travail vise plus à vérifier la solidité de parties plus avancées du système de type qu'à couvrir l'ensemble des fonctionnalités des programmes OCaml existants. Je pense qu'en termes d'essayer de prouver l'exactitude d'un programme OCaml existant, CFML serait un meilleur choix.

gasche
la source