Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/6563
Título: | Pointfree factorization of operation refinement |
Autor(es): | Oliveira, José Nuno Fonseca Rodrigues, César J. |
Palavras-chave: | Theoretical foundations Refinement Calculation Reusable theories |
Data: | 2006 |
Editora: | Springer |
Revista: | Lecture Notes in Computer Science |
Citação: | Oliveira, J.N., Rodrigues, C.J. (2006). Pointfree Factorization of Operation Refinement. In: Misra, J., Nipkow, T., Sekerinski, E. (eds) FM 2006: Formal Methods. FM 2006. Lecture Notes in Computer Science, vol 4085. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11813040_17 |
Resumo(s): | The standard operation refinement ordering is a kind of “meet of op- posites”: non-determinism reduction suggests “smaller” behaviour while increase of definition suggests “larger” behaviour. Groves’ factorization of this ordering into two simpler relations, one per refinement concern, makes it more mathe- matically tractable but is far from fully exploited in the literature. We present a pointfree theory for this factorization which is more agile and calculational than the standard set-theoretic approach. In particular, we show that factorization leads to a simple proof of structural refinement for arbitrary parametric types and ex- ploit factor instantiation across different subclasses of (relational) operation. The prospect of generalizing the factorization to coalgebraic refinement is discussed |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/6563 |
ISBN: | 978-3-540-37215-8 |
e-ISBN: | 978-3-540-37216-5 |
DOI: | 10.1007/11813040_17 |
ISSN: | 0302-9743 |
Acesso: | Acesso aberto |
Aparece nas coleções: | DI/CCTC - Artigos (papers) |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
paper_jno.pdf | Documento principal | 195,79 kB | Adobe PDF | Ver/Abrir |