RT Journal Article
T1 Extending Liquid Types to Arrays
A1 Montenegro Montes, Manuel
A1 Nieva Soto, Susana
A1 Peña Marí, Ricardo Vicente
A1 Segura Díaz, Clara María
AB A liquid type is an ordinary Hindley-Milner type annotated with a logical predicate that states the properties satisfied by the elements of that type. Liquid types are a powerful tool for program verification, since programmers can use them to specify pre- and postconditions of their programs, while the predicates of intermediate variables and auxiliary functions are inferred automatically. Type inference is feasible in this context, since the logical predicates within liquid types are constrained to a quantifier-free logic in order to maintain decidability.In this paper we extend liquid types by allowing them to contain quantified properties on arrays, so that they can be used to infer invariants on array-related programs (for example, implementations of sorting algorithms). Although quantified logic is, in general, undecidable, we restrict properties on arrays to a decidable subset introduced by Bradley et al. We describe in detail the extended type system, the verification condition generator, and the iterative weakening algorithm for inferring invariants. After proving the correctness and completeness of these two algorithms, we apply them to find invariants on a set of algorithms involving array manipulations.
PB ACM
SN 1529-3785
YR 2020
FD 2020-01-21
LK https://hdl.handle.net/20.500.14352/7066
UL https://hdl.handle.net/20.500.14352/7066
LA eng
NO Ministerio de Economía y Competitividad (MINECO)
NO Comunidad de Madrid/FEDER
DS Docta Complutense
RD 16 abr 2025