Reasoning about static and dynamic properties in Alloy : (Record no. 52348)

MARC details
000 -CABECERA
campo de control de longitud fija 02832naa a2200265 a 4500
003 - IDENTIFICADOR DEL NÚMERO DE CONTROL
campo de control AR-LpUFIB
005 - FECHA Y HORA DE LA ÚLTIMA TRANSACCIÓN
campo de control 20250311170245.0
008 - DATOS DE LONGITUD FIJA--INFORMACIÓN GENERAL
campo de control de longitud fija 230201s2005 xx o 000 0 eng d
024 8# - Otro identificador estandar
Número estándar o código DIF-M2561
-- 2651
-- DIF002463
040 ## - FUENTE DE LA CATALOGACIÓN
Centro catalogador/agencia de origen AR-LpUFIB
Lengua de catalogación spa
Centro/agencia transcriptor AR-LpUFIB
100 1# - ENTRADA PRINCIPAL--NOMBRE DE PERSONA
Nombre de persona Frias, Marcelo F.
245 10 - MENCIÓN DE TÍTULO
Título Reasoning about static and dynamic properties in Alloy :
Resto del título A purely relational approach
490 0# - MENCIÓN DE SERIE
Mención de serie ^p Datos electrónicos (1 archivo : 412 KB)
500 ## - NOTA GENERAL
Nota general Formato de archivo: PDF. -- Este documento es producción intelectual de la Facultad de Informática-UNLP (Colección BIPA / Biblioteca.) -- Disponible también en línea (Cons. 19/12/2008)
520 ## - SUMARIO, ETC.
Sumario, etc. We study a number of restrictions associated with the first-order relational specification language Alloy. The main shortcomings we address are: -the lack of a complete calculus for deduction in Alloy's underlying formalism, the so called relational logic, -the inappropriateness of the Alloy language for describing (and analyzing) properties regarding execution traces. The first of these points was not regarded as an important issue during the genesis of Alloy, and therefore has not been taken into account in the design of the relational logic. The second point is a consequence of the static nature of Alloy specifications, and has been partly solved by the developers of Alloy; however, their proposed solution requires a complicated and unstructured characterization of executions. We propose to overcome the first problem by translating relational logic to the equational calculus of fork algebras. Fork algebras provide a purely relational formalism close to Alloy, which possesses a complete equational deductive calculus. Regarding the second problem, we propose to extend Alloy by adding actions. These actions, unlike Alloy functions, do modify the state. Much the same as programs in dynamic logic, actions can be sequentially composed and iterated, allowing them to state properties of execution traces at an appropriate level of abstraction. Since automatic analysis is one of Alloy's main features, and this article aims to provide a deductive calculus for Alloy, we show that: -the extension hereby proposed does not sacrifice the possibility of using SAT solving techniques for automated analysis, -the complete calculus for the relational logic is straightforwardly extended to a complete calculus for the extension of Alloy.
534 ## - NOTA SOBRE LA VERSIÓN ORIGINAL
Encabezamiento principal del original (2005) ACM Transactions on Software Engineering and Methodology, 14 (4), pp. 478-526.
650 #4 - PUNTO DE ACCESO ADICIONAL DE MATERIA--TÉRMINO DE MATERIA
Término de materia o nombre geográfico como elemento de entrada VERIFICACIÓN DE PROGRAMAS
650 #4 - PUNTO DE ACCESO ADICIONAL DE MATERIA--TÉRMINO DE MATERIA
Término de materia o nombre geográfico como elemento de entrada MÉTODOS FORMALES
700 1# - PUNTO DE ACCESO ADICIONAL--NOMBRE DE PERSONA
Nombre de persona Maibaum, Thomas S. E.
700 1# - PUNTO DE ACCESO ADICIONAL--NOMBRE DE PERSONA
Nombre de persona Aguirre, Nazareno M.
700 1# - PUNTO DE ACCESO ADICIONAL--NOMBRE DE PERSONA
Nombre de persona Baum, Gabriel Alfredo
700 1# - PUNTO DE ACCESO ADICIONAL--NOMBRE DE PERSONA
Nombre de persona López Pombo, Carlos G.
856 40 - LOCALIZACIÓN Y ACCESO ELECTRÓNICOS
Identificador Uniforme del Recurso <a href="www.lifia.info.unlp.edu.ar/papers/2005/Frias2005.pdf">www.lifia.info.unlp.edu.ar/papers/2005/Frias2005.pdf</a>
942 ## - ELEMENTOS DE PUNTO DE ACCESO ADICIONAL (KOHA)
Tipo de ítem Koha Capítulo de libro
Holdings
Estado de retiro Estado de pérdida Estado dañado Disponibilidad Colección Biblioteca permanente Biblioteca actual Fecha de adquisición Total de préstamos Signatura topográfica completa Fecha visto por última vez Identificador Uniforme del Recurso Precio válido a partir de Tipo de ítem Koha
      No corresponde Biblioteca digital Biblioteca de la Facultad de Informática Biblioteca de la Facultad de Informática 11/03/2025   A0079 11/03/2025 http://catalogo.info.unlp.edu.ar/meran/getDocument.pl?id=83 11/03/2025 Capítulo de libro