Autor:
Nieva, Susana

Foto de perfil

E-mails conocidos

nieva@sip.ucm.es

Fecha de nacimiento

Proyectos de investigación

Unidades organizativas

Puesto de trabajo

Apellidos

Nieva

Nombre de pila

Susana

Nombre

Nombres alternativos

Afiliaciones conocidas

Complutense University of Madrid, Spain
Facultad de Informática Universidad Complutense de Madrid, Spain

Páginas web conocidas

Página completa del ítem
Notificar un error en este autor

Filtros

2015 - 20162
Restablecer filtros

Ajustes

Resultados de la búsqueda

Mostrando 1 - 2 de 2
  • Miniatura
    Artículo
    HR-SQL: An SQL Database System with Extended Recursion and Hypothetical Reasoning
    Nieva, Susana; Saenz-Perez, Fernando; Sánchez-Hernández, Jaime. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
    In a former work we described the system and language R-SQL that overcomes some limitations of recursion of the relational database language SQL. Such limitations are non-linearity, mutual recursion, and some combinations of negation with recursion. In addition, R-SQL improved termination properties of recursive definitions. Next, this language was extended to include a restricted form of hypothetical relations and queries using assumptions, obtaining the language HR-SQL, and a preliminary implementation was developed for it. Here, we develop a new system HR-SQL from scratch and enhance the former system in several areas. First, hypothetical reasoning is fully integrated with recursive definitions. Second, the Python script generated by the system for computing the extension (materialization) of a database is now targeted to several state-of-the-art relational database systems. Third, the system has been interfaced to the integrated development environment ACIDE, allowing both a more friendly user interaction and a graphical view of the dependency graph that shows dependencies between relations. Fourth, being developed in Prolog, we have targeted it to both SICStus Prolog and SWI-Prolog, also providing standalone executables. Finally, the system has been extended with a bundle of commands, highly improving its capabilities with respect to the former system.
  • Miniatura
    Artículo
    Synthesizing Invariants for Arrays
    Montenegro, Manuel; Nieva, Susana; Peña Marí, Ricardo; Segura, Clara. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.
    Liquid types can be seen as as a computer assisted verification system. Ordinary Hindley-Milner types are qualified by predicates expressing properties. In this way, the programmer may specify the preconditions and postconditions of functions. More importantly, the system infers the types of all the intermediate variables and checks that the verification conditions proving correctness hold. The predicates are currently expressed in a quantifier free decidable logic. Here, we extend Liquid types with quantified predicates of a decidable logic for arrays, propose a concept of an array refinement type, and provide an inference algorithm for this extension. By applying this ideas to several imperative algorithms dealing with arrays, we have been able to infer complex invariants.