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: | MISRA, Jayadev ; NIPKOW, Tobias ; SEKERINSKI, Emil, ed. lit. – “FM 2006 : proceedings of the International Symposium on Formal Methods, 14, Hamilton, Canada, 2006”. Berlin : Springer, 2006. ISBN 3-540-37215-6. p. 236-251. |
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: | 3-540-37215-6 |
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 |