Miscelánea
URI permanente para esta colección:
Artículos en la categoría Miscelánea publicados en las Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023).
Notificar un error en esta colección
Examinar
Envíos recientes
Artículo Indecidibilidad del análisis de dependencias de datosGalindo, Carlos; Pérez Rubio, Sergio; Sílva, Josep. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.Los análisis de dependencias de datos (ADD) responden a la pregunta: ¿qué partes del programa pueden influenciar el valor de esta variable? Estos análisis son comunes en herramientas como compiladores, depuradores y muchos otros análisis de software para determinar terminación, paralelizar automáticamente, depurar, optimizar, etc. Sabemos que en el caso general ADD es indecidible debido a la no-terminación: siempre es posible encontrar un programa para el que no podemos asegurar si la variable de interés es alcanzable (el programa podría divergir antes), y por tanto no podemos determinar si alguna parte del programa podría influenciar a esa variable. En enero del 2000, Thomas Reps probó la indecidibilidad de un ADD para programas que sí terminan, demostrando que la no-terminación no es la única causa fundamental de indecidibilidad. El ADD que Reps utilizó, sin embargo, era un análisis muy específico. Este trabajo utiliza y expande los resultados de Reps para determinar que existe una clase de ADDs (que incluye el propio ADD usado por Reps) que son indecidibles incluso para programas que sí terminan. Además, describimos qué características debe tener un lenguaje de programación para que los ADDs de esta clase sean indecidibles en el caso general.Artículo Nostralangus: Prophecy-based programmingCeresa, Martin; Sánchez, César. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.In this work in progress, we explore the possibility of having a new operator capable of bringing information about the system in the future. While previous works define \emph{prophecy variables} as a way of inspecting the state of the system in the future, we propose to write programs that can actively use such information to choose what agents can do now. Verification techniques define systems where no \textbf{paradoxes} can be introduced but information from the future is still accessible to us as verifiers. In this document, we liberate the programs of such restriction equipping programs with a prophetic conditional operation: \(\ \, \mathcal{P}(\Phi) \, \ \, \mathcal{A} \, \ \, \mathcal{B}\). Actions \(\mathcal{A}\) and \(\mathcal{B}\) are executed depending on a future predicate \(\Phi\) about the system. Both sets of actions \(\mathcal{A}\) and \(\mathcal{B}\) can contradict the prophecy creating paradoxes. We explore how we can rule out some paradoxes appealing to different execution systems and two interpretations of prophecies. One of \emph{possible worlds} where making a prediction generates two possible worlds, one on which the prediction is true and another on which is false. Another interpretation in which the time is linearized using a try-catch interpretation.Resumen Executable Contracts for ElixirPérez Rubio, Sergio; Bueso de Barrio, Luis Eduardo; Ballesteros González, Ignacio; Herranz, Angel; Mariño, Julio; Benac Earle, Clara; Fredlund, Lars-Ake. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.This paper introduces a new library for implementing executable contracts in Elixir. In addition to classical contract constructs such as preconditions and postconditions, the library permits e.g. to specify exceptional behaviour (i.e. which exceptions are thrown and under which conditions), and to associate timers with function calls to detect non-terminating or too slow computations.