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

• Type: Article in International Conference Proceedings Book
• Date: 2012

Authors

Macedo, N (Author) Other; Pacheco, H (Author) Other; Cunha, A (Author) Other

Conference proceedings International

Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Pages: 146-161

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

Cambridge, 17 September 2012 through 20 September 2012

Indexing

Scopus - 2 Citations

Other information

Authenticus ID: 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.

Language: English

Type (Professor's evaluation): Scientific