Refinamento (computação)

Refinamento é um termo genérico da ciência da computação que abrange várias abordagens para produzir programas de computador corretos e simplificar programas existentes para permitir sua verificação formal.

Refinamento do programa

Nos métodos formais , o refinamento do programa é a transformação verificável de uma especificação formal abstrata (de alto nível) em um programa executável concreto (de baixo nível) . [ citação necessária O refinamento gradual permite que esse processo seja feito em etapas. Logicamente, o refinamento normalmente envolve implicação , mas pode haver complicações adicionais.

A preparação progressiva just-in-time do backlog do produto (lista de requisitos) em abordagens ágeis de desenvolvimento de software , como Scrum , também é comumente descrita como refinamento. [1]

Refinamento de dados

O refinamento de dados é usado para converter um modelo de dados abstrato (em termos de conjuntos , por exemplo) em estruturas de dados implementáveis ​​(como arrays ). [ citação necessária O refinamento da operação converte uma especificação de uma operação em um sistema em um programa implementável (por exemplo, um procedimento ). A pós-condição pode ser fortalecida e/ou a pré-condição enfraquecida neste processo. Isto reduz qualquer não-determinismo na especificação, normalmente para uma implementação completamente determinística .

Por exemplo, x ∈ {1,2,3} (onde x é o valor da variável x após uma operação) poderia ser refinado para x ∈ {1,2}, então x ∈ {1}, e implementado como x  : = 1. Implementações de x  := 2 e x  := 3 seriam igualmente aceitáveis ​​neste caso, usando uma rota diferente para o refinamento. Entretanto, devemos ter cuidado para não refinar para x ∈ {} (equivalente a false ), pois isso não é implementável; é impossível selecionar um membro do conjunto vazio .

O termo reificação também é algumas vezes usado (cunhado por Cliff Jones ). A contenção é uma técnica alternativa quando o refinamento formal não é possível. O oposto do refinamento é a abstração .

Cálculo de refinamento

O cálculo de refinamento é um sistema formal (inspirado na lógica de Hoare ) que promove o refinamento do programa. O Sistema de Transformação FermaT é uma implementação de refinamento com força industrial. O Método B também é um método formal que estende o cálculo de refinamento com uma linguagem componente: tem sido usado em desenvolvimentos industriais.

Tipos de refinamento

Na teoria dos tipos , um tipo de refinamento [2] [3] [4] é um tipo dotado de um predicado que se presume ser válido para qualquer elemento do tipo refinado. Os tipos de refinamento podem expressar pré-condições quando usados ​​como argumentos de função ou pós-condições quando usados ​​como tipos de retorno : por exemplo, o tipo de função que aceita números naturais e retorna números naturais maiores que 5 pode ser escrito como . Os tipos de refinamento estão, portanto, relacionados à subtipagem comportamental .

Veja também

Referências

  1. ^ Cho, eu (2009). “Adotando uma cultura ágil, a jornada da equipe de experiência do usuário” . Conferência Ágil de 2009 . págs. doi :10.1109/AGILE.2009.76. ISBN 978-0-7695-3768-9. S2CID38580329  .
  2. ^ Freeman, T.; Pfenning, F. (1991). "Tipos de refinamento para ML" (PDF) . Anais da Conferência ACM sobre Design e Implementação de Linguagem de Programação . páginas 268–277. doi :10.1145/113445.113468.
  3. ^ Hayashi, S. (1993). “Lógica dos tipos de refinamento”. Anais do Workshop sobre Tipos de Provas e Programas . páginas 157–172. CiteSeerX 10.1.1.38.6346 . doi :10.1007/3-540-58085-9_74. 
  4. ^ Denney, E. (1998). “Tipos de refinamento para especificação”. Anais da Conferência Internacional IFIP sobre Conceitos e Métodos de Programação . Vol. 125. Chapman & Salão. páginas 148–166. CiteSeerX 10.1.1.22.4988 . 


Retrieved from "https://en.wikipedia.org/w/index.php?title=Refinement_(computing)&oldid=1215731572"