En la cuarta parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones a los ejercicios de la relación 17 sobre mayorías parlamentarias como caso de estudio de tipos algebraicos.
Los ejercicios y su solución se muestran a continuación
Read More “I1M2015: Mayorías parlamentarias”
En la tercera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones a los ejercicios de la relación 16 sobre el uso de números aleatorios para calcular el número π mediante el método de Montecarlo.
Los ejercicios y su solución se muestran a continuación
Read More “I1M2015: Cálculo del número pi mediante el método de Montecarlo”
En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones a los ejercicios de la relación 15 sobre el uso de acciones de entrada y salida en el juego del Nim.
Los ejercicios y su solución se muestran a continuación
Read More “I1M2015: El juego del Nim y las funciones de entrada/salida”
En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentando las soluciones del 9º ejercicio de la 14ª relación sobre el triángulo de Floyd.
Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2015: El triángulo de Floyd”
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Software component design with the B method: a formalization in Isabelle/HOL.
Sus autores son
Su resumen es
This paper presents a formal development of an Isabelle/HOL theory for the behavioral aspects of artifacts produced in the design of software components with the B method. We first provide a formalization of semantic objects such as labelled transition systems and notions of behavior and simulation. We define an interpretation of the B method using such concepts. We also address the issue of component composition in the B method.
El trabajo se ha presentado en FACS 2015 (12th Intl. Conf. Formal Aspects of Component Software).
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.
Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.