In situ Enhancement of Type Safety using Fictive Types

Richárd, Szalay [Szalay, Richárd (Programozási nyel...), szerző] Programozási Nyelvek és Fordítóprogramok Tanszék (ELTE / IK); PhD Informatika Doktori Iskola (ELTE / IK); Ábel, Sinkovics [Sinkovics, Ábel (Informatika), szerző]; Zoltán, Porkoláb [Porkoláb, Zoltán (Programozási nyel...), szerző] Programozási Nyelvek és Fordítóprogramok Tanszék (ELTE / IK)

Angol nyelvű Absztrakt / Kivonat (Egyéb konferenciaközlemény) Tudományos
    • MTMT: 31620652
    Type systems are a crucial tool in the hands of software developers for ensuring an increased level of soundness to their programs, and to guard against bugs. However, in many cases, the type systems are not used to their full capabilities, and trade-offs are made. One infamous accident that resulted from the lack of type safety is the case of the exploded Mars probe [6], where developers using both metric and imperial measurements mixed these values without annotating the unit, leading to excessive throttling which caused the accident. Various widely used programming languages, such as C++, Java, Python, Rust are yet to implement constrained types as a language feature. In most cases, constrained types, which are the easiest way to ensure a unit-aware type system might only exist as libraries, such as for C++. Extensive type systems are readily available in functional programming languages, however, with the convergence of paradigms and the availability of functional elements in traditionally object-oriented or imperative languages [1], it is a reasonable expectation to raise the level of safety expected from software. C++ has supported compile-time functional programming elements through template metaprogramming [4], but ensuring both compile-time validation of operations and run-time validation of data is not possible automatically. While user-defined types are common in modern languages that support such notion, developers resort to using the most conceptually fundamental types, such as int or string, as they are, and not associating any “strong type” [3] to range-constrained integers. The goal of refactoring efforts is to produce equivalent software that is “better” by some metric or idea. Simply defining a new type and changing a program element’s type to this new type is not sufficient, as the code will break due to not defined operations and conversions. A non-compiling state of the project is detrimental, as the refactoring tools often rely on the code being in an invariant-compliant state, and thus can not be used anymore. As such, incremental refactoring is needed [7]. This can be achieved primarily by investigating the landscape and finding offending types and creating automated rules that refactor the code based on previously explored knowledge. Such an effort works for unit-based systems, such as timekeeping [8] or physics [5]. In this paper, we investigate an incremental approach that uses code annotations. The upside of the approach is that information encoded in annotations can be easily understood by tools without changing the semantics of the code at hand. Previously, type migration has been done in a well-scaling manner between already existing types [2]. We propose a method by which the developer can paint a particular program element (of any type in the type system, e.g. int) with an annotation, which will be propagated by tools across the software project. Until this propagation is done, the existing code is not altered and can still be compiled and developed. Once the propagation has finished, the insight gained from the operations required on this fledgeling type (e.g.velocity) can be reviewed, and the new type can be generated. Afterwards, usage points are rewritten to this new type.
    Hivatkozás stílusok: IEEEACMAPAChicagoHarvardCSLMásolásNyomtatás
    2022-09-27 23:50