Archive | décembre 2018

Clang-tidy

Au bureau, on nous a cédé le code source d’un logiciel relativement ancien et dont le précédent propriétaire ne souhaitait pas continuer la maintenance.Si d’ m point de vue business il s’ agissait d’une opportunité des plus lucratives, puisqu’on a hérité d’une base de clients colossales, travailler sur du code qui a dormi parfois pendant près de 10 ans est particulièrement difficile.

Pour dresser une image plus précise, le projet utilise une version antédiluvienne de WxWidgets et de boost, en réimplémentant toutefois les smart pointers (qui étaient probablement encore à l’état de standardisation à l’époque ). On ressent assez rapidement le fait que plusieurs personnes sont passés dessus, avec un étrange mélange de pratique douteuses de développement logiciel (des fichiers entiers copié et collés) qui côtoient les design pattern classiques d’une base de code de taille respectable.

Et bien entendu, il n’y a pas ou peu de tests unitaires rendant chaque tentative de refactoring hasardeuse.

La récente série de posts autour de la customisation de clang-tidy sur le blog de visual c++ tombe à bien nommé :

  • https://blogs.msdn.microsoft.com/vcblog/2018/10/19/exploring-clang-tooling-part-1-extending-clang-tidy/
  • https://blogs.msdn.microsoft.com/vcblog/2018/10/23/exploring-clang-tooling-part-2-examining-the-clang-ast-with-clang-query/
  • https://blogs.msdn.microsoft.com/vcblog/2018/11/06/exploring-clang-tooling-part-3-rewriting-code-with-clang-tidy/

Pour référence pour plus tard je partage le bout de code qui permet de détecter les types std::string, qu’ils apparaissent explicitement ou via un using ou typedef:

auto typeParamMatcher =
		varDecl(hasType(hasUnqualifiedDesugaredType(
     recordType(hasDeclaration(cxxRecordDecl(hasName("basic_string")))))));

Si on supprime le hasUnqualifiedDesugaredType, on peut ne matcher que l’apparition explicite de ce type:

varDecl(hasType(cxxRecordDecl(matchesName("string"))))

Intérieurs et adhérences en Coq

On continue dans la série d’exercice autour de la topologie, cette fois-ci en rentrant un peu plus dans le sujet en manipulant les concepts d’intérieur et d’adhérence.
Le module coq topology fournit une définition de ces concepts, ainsi que plusieurs propriétés usuelles (inclusions diverses, relation avec les compléments, caractérisation par la rencontre non vide etc) ; j’ai senti moins d’absences étranges que dans le cas des unions de familles comme dans les 2 exercices précédents.

Le sujet, toujours tiré de la même feuille d’exercice :

Si \(A\) est une partie de l’espace topologique \(X\), on pose \(\alpha(A) = \mathring{\overline{A}}\) et \(\beta(A) = \overline{\mathring{A}}\).
Montrer que \(\alpha\) et \(\beta]\) sont des applications croissantes pour l’inclusion de \(\mathcal{P}(X)\) dans \(\mathcal{P}(X)\).
Montrer que si \(A\) est ouvert, \(A\subset\alpha(A)\) et si \(A\) est fermé, \(\beta(A)\subset A\). En déduire que
\(\alpha^2 = \alpha\) et \(\beta^2 = \beta\).

On va traduire les définitions en Coq :

From Topology Require Import InteriorsClosures. 

Definition alpha (X:TopologicalSpace) (A:Ensemble (point_set X)) :=
interior (closure A). 

Definition beta (X:TopologicalSpace) (A:Ensemble (point_set X)) := 
closure (interior A).

La croissance est relativement facile à prouver à partir de la croissance des intérieurs fourni par le module topology et adhérences et en tripatouillant les définitions :

Theorem croiss (X:TopologicalSpace) :
    forall A B, Included A B -> Included (alpha X A) (alpha X B).
Proof.
   unfold alpha. unfold Included. intros A B H x.
   apply interior_increasing. apply closure_increasing.
   unfold Included. apply H.
Qed.

Prouver les inclusions est également relativement simple :

Theorem open_alpha (X:TopologicalSpace) :
    forall A: Ensemble (point_set X), open A -> Included A (alpha X A). Proof.
    unfold alpha. intros. Search (interior). apply interior_maximal.
    apply H. apply closure_inflationary.
Qed.

Theorem closure_beta (X:TopologicalSpace) :
    forall A: Ensemble (point_set X), closed A -> Included (beta X A) A.
Proof.
   unfold beta. intros. Search (closure). apply closure_minimal.
   apply H. Search (interior). apply interior_deflationary.
Qed.

La dernière propriété est un peu plus délicate à prouver. Déplier les définitions n’est pas suffisant… Il faut en effet reconnaitre \(\alpha\) dans l’expression de \(\beta^2\) et réciproqement pour appliquer la propriété précédente.

Require Import Coq.Logic.FunctionalExtensionality. 

Theorem alpha_square (X:TopologicalSpace):
    alpha X = fun A => alpha X (alpha X A).
Proof.
   apply functional_extensionality. intros.
   apply Extensionality_Ensembles. unfold Same_set. split.
   - apply open_alpha. Search (interior). apply interior_open.
   - unfold alpha in *. pose(tmp:=closure_beta X (closure x)).
       unfold beta in tmp. Search (interior).
       apply interior_increasing. apply tmp. apply closure_closed.
 Qed.