Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Core Calculus for Type-safe Product Lines of C Programs

Ferruccio Damiani, Daisuke Kimura, Luca Paolini, Makoto Tatsuta

TL;DR

A core calculus that formalizes a proper subset of the ANSI C without preprocessor directives is proposed and a type system is defined for CLC that guarantees that all programs to be generated by the C preprocessor are well-typed C programs.

Abstract

In this paper we: (1) propose Lightweight C (LC), namely a core calculus that formalizes a proper subset of the ANSI C without preprocessor directives; (2) define Colored LC (CLC), namely LC endowed with ANSI C preprocessor directives; and (3) define a type system for CLC that guarantees that all programs to be generated by the C preprocessor are well-typed C programs. We believe that the simple formalization provided by CLC could be useful also for teaching purposes. Stefano Berardi spent most of his academic career at the Department of Computer Science of the University of Turin, where he conducts outstanding research on the logical foundations of computer science and on type-based program analyses. Over the years, he taught many courses, from BSc courses on programming with C to PhD courses on program analysis. Therefore, this paper fully falls within Stefano Berardi's research and teaching activities.

A Core Calculus for Type-safe Product Lines of C Programs

TL;DR

A core calculus that formalizes a proper subset of the ANSI C without preprocessor directives is proposed and a type system is defined for CLC that guarantees that all programs to be generated by the C preprocessor are well-typed C programs.

Abstract

In this paper we: (1) propose Lightweight C (LC), namely a core calculus that formalizes a proper subset of the ANSI C without preprocessor directives; (2) define Colored LC (CLC), namely LC endowed with ANSI C preprocessor directives; and (3) define a type system for CLC that guarantees that all programs to be generated by the C preprocessor are well-typed C programs. We believe that the simple formalization provided by CLC could be useful also for teaching purposes. Stefano Berardi spent most of his academic career at the Department of Computer Science of the University of Turin, where he conducts outstanding research on the logical foundations of computer science and on type-based program analyses. Over the years, he taught many courses, from BSc courses on programming with C to PhD courses on program analysis. Therefore, this paper fully falls within Stefano Berardi's research and teaching activities.
Paper Structure (18 sections, 8 theorems, 3 equations, 12 figures)

This paper contains 18 sections, 8 theorems, 3 equations, 12 figures.

Table of Contents

  1. Introduction
  2. Background and Related Work
  3. Background
  4. Related Work
  5. On Core Languages for C
  6. On Core Calculi for the Annotative Approach to SPL Implementation
  7. Running Example
  8. Lightweight C
  9. LC Syntax
  10. LC Typing
  11. Colored Lightweight C
  12. CLC Syntax
  13. CLC Typing
  14. Variant Generation
  15. Properties
  16. ...and 3 more sections

Key Result

Theorem 6.1

Consider a CLC SPL $(\Phi,Prg, \textsc{at}\ )$ with $\Phi=(\mathcal{F},\phi)$. If $\phi\vdash Prg \; \textsc{ok}$ then $\vdash Prg \; \textsc{ok}$.

Figures (12)

  • Figure 1: Variant 1 (for product $p_1 = \emptyset$) of the Queue SPL.
  • Figure 2: Variant 2 (for product $p_2 = \{\}$) of the Queue SPL.
  • Figure 3: Variants 3 (for $p_3 = \{\}$) and 4 (for $p_4 = \{, \}$) of the Queue SPL.
  • Figure 4: Variants 5 (for $p_5 = \{, \}$) and 6 ($p_6 = \{, , \}$) of the Queue SPL.
  • Figure 5: Code base of the Queue SPL, where the code associated to the annotations LAST, OCCURS, INTERVAL, !LAST, and LAST && !LAST (i.e., false) is highlighted with different colors.
  • ...and 7 more figures

Theorems & Definitions (27)

  • Definition 2.1: FM in propositional representation
  • Remark 2.2: On the syntax used for the proposition formulas
  • Remark 3.1: A couple of annotative C SPL programming patterns
  • Remark 4.1: On the syntax of LC and the syntax of ANSI C
  • Example 4.2: Some LC programs
  • Example 4.3: Some well-typed LC programs
  • Remark 5.1: On the CLC annotation table and the #if preprocessor directives
  • Remark 5.2: Syntactic sugar for the CLC annotation table
  • Example 5.3: The Queue SPL
  • Example 5.5: Family-based typing of the Queue SPL
  • ...and 17 more