2026-06-27T11:25:08Zhttps://docta.ucm.es/rest/oai/request

oai:docta.ucm.es:20.500.14352/70662024-08-21T14:48:12Zcom_20.500.14352_14col_20.500.14352_15

00925njm 22002777a 4500 dc Montenegro Montes, Manuel author Nieva Soto, Susana author Peña Marí, Ricardo Vicente author Segura Díaz, Clara María author 2020-01-21 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. 1529-3785 10.1145/3362740 https://hdl.handle.net/20.500.14352/7066 https://dl.acm.org/doi/10.1145/3362740 Extending Liquid Types to Arrays