Static Type Analysis of Pattern Matching by Abstract Interpretation - Formal Techniques for Distributed Systems
Conference Papers Year : 2010

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.
Fichier principal
Vignette du fichier
61170183.pdf (194.08 Ko) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

hal-01055154 , version 1 (11-08-2014)

Licence

Identifiers

Cite

Pietro Ferrara. Static Type Analysis of Pattern Matching by Abstract Interpretation. 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. pp.186-200, ⟨10.1007/978-3-642-13464-7_15⟩. ⟨hal-01055154⟩
162 View
286 Download

Altmetric

Share

More