Relations as Executable Specifications: Taming Partiality and Non-determinism Using Invariants

• Tipo: Artigo em Livro de Atas de Conferência Internacional
• Data: 2012

Autores

Macedo, N (Autor) Outra; Pacheco, H (Autor) Outra; Cunha, A (Autor) Outra

Ata de Conferência Internacional

Título: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Páginas: 146-161

13th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2012

Cambridge, 17 September 2012 through 20 September 2012

Indexação

Scopus - 2 Citações

Outras Informações

ID Authenticus: P-008-6SE

DOI: 10.1007/978-3-642-33314-9_10

Abstract (EN): The calculus of relations has been widely used in program specification and reasoning. It is very tempting to use such specifications as running prototypes of the desired program, but, even considering finite domains, the inherent partiality and non-determinism of relations makes this impractical and highly inefficient. To tame partiality we prescribe the usage of invariants, represented by coreflexives, to characterize the exact domains and codomains of relational specifications. Such invariants can be used as pre-condition checkers to avoid runtime errors. Moreover, we show how such invariants can be used to narrow the non-deterministic execution of relational specifications, making it viable for a relevant class of problems. In particular, we show how the proposed techniques can be applied to execute specifications of bidirectional transformations, a domain where partiality and non-determinism are paramount. © 2012 Springer-Verlag.

Idioma: Inglês

Tipo (Avaliação Docente): Científica