Framework para el Desarrollo de Software mediante Modularización Avanzada. 2da. Etapa

Permanent URI for this collection

https://repositorio.uai.edu.ar/handle/123456789/295

Browse

Browsing Framework para el Desarrollo de Software mediante Modularización Avanzada. 2da. Etapa by Author "Rosenfeld, Ricardo Fabián"
  • Item
    Introducción a la verificación de programas
    (Universidad Abierta Interamericana. Facultad de Tecnología Informática, 2022-6) Rosenfeld, Ricardo Fabián
    Iniciamos una serie de cuatro artículos introductorios sobre la verificación axiomática de programas, en el marco de los programas imperativos de entrada/salida. En este artículo introducimos el método axiomático de verificación para los programas secuenciales determinísticos, y desarrollamos ejemplos de aplicación. Si bien la verificación de programas se expone como una actividad a posteriori (dados un programa y una especificación, verificar que el programa satisface la especificación), la idea que se sostiene en el artículo, y en toda la serie, es tener en cuenta los axiomas y reglas del método para programar al mismo tiempo que verificar, de modo tal de obtener programas correctos por construcción. Con esta perspectiva, al final se ejemplifica un desarrollo sistemático de programa basado en la axiomática presentada.
  • Item
    Verificación de programas no determinísticos
    (Universidad Abierta Interamericana. Facultad de Tecnología Informática, 2022-12) Rosenfeld, Ricardo Fabián
    Continuando con nuestra serie de artículos introductorios sobre la verificación axiomática de programas, en este segundo trabajo nos enfocamos en el paradigma secuencial no determinístico, siempre en el marco de los programas imperativos de entrada/salida. Como el no determinismo se manifiesta en la concurrencia, el artículo sirve también como introducción a la verificación de programas concurrentes, en los que más se justifica por su complejidad un tratamiento formal de las pruebas de correctitud. Trabajamos con un clásico lenguaje de programación, con selección condicional y repetición no determinísticas, al que luego se incorporan asignaciones aleatorias. Para las pruebas de los programas planteamos una adaptación del método axiomático de verificación descripto en la publicación previa, limitado a la programación secuencial determinística. Presentamos ejemplos de aplicación del método e incluimos un desarrollo sistemático de programa, volviendo a destacar el approach de utilizar los axiomas y reglas para programar al mismo tiempo que verificar, con el objeto de obtener programas correctos por construcción. Finalmente introducimos el concepto de fairness, cuyo efecto es reducir el grado de no determinismo de un programa en base a determinados criterios de equidad en el entorno de ejecución, y describimos un par de adaptaciones en las reglas de prueba para contemplar este aspecto.