Static Type Analysis of Pattern Matching by Abstract Interpretation

Abstract : Pattern matching is one of the most attractive features of functional programming languages. Recently, pattern matching has been applied to programming languages supporting the main current object oriented features. In this paper, we present a static type analysis based on the abstract interpretation framework aimed at proving the exhaustiveness of pattern matchings and the safety of type casts. The analysis is composed by two distinct abstract domains. The first domain collects information about dynamic typing, while the second one tracks the types that an object cannot be instance of. The analysis has been implemented and applied to all the Scala library. The experimental results underline that our approach scales up since it analyzes a method in 90 msec in average. In addition, the analysis is precise in practice as well, since we prove the exhaustiveness of 42% of pattern matchings and 27% of the type casts without any manual annotation on the code.
Type de document :
Communication dans un congrès
John Hatcliff; Elena Zucca. Joint 12th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 30th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2010, Amsterdam, Netherlands. Springer, Lecture Notes in Computer Science, LNCS-6117, pp.186-200, 2010, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-13464-7_15〉
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01055154
Contributeur : Hal Ifip <>
Soumis le : lundi 11 août 2014 - 16:30:16
Dernière modification le : vendredi 11 août 2017 - 16:16:21
Document(s) archivé(s) le : mercredi 26 novembre 2014 - 22:15:31

Fichier

61170183.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Pietro Ferrara. Static Type Analysis of Pattern Matching by Abstract Interpretation. John Hatcliff; Elena Zucca. Joint 12th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 30th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2010, Amsterdam, Netherlands. Springer, Lecture Notes in Computer Science, LNCS-6117, pp.186-200, 2010, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-13464-7_15〉. 〈hal-01055154〉

Partager

Métriques

Consultations de la notice

228

Téléchargements de fichiers

101