ARepair: Uma Estrutura de Reparação para Alloy

Pesquisadores propuseram muitas técnicas automatizadas de reparação de programas para linguagens imperativas, como Java. No entanto, poucos trabalhos foram feitos para reparar programas escritos em linguagens declarativas, como Alloy. Nós propusemos o ARepair, a primeira técnica automatizada de reparação de programas para modelos defeituosos de Alloy. O ARepair recebe como entrada um modelo defeituoso de Alloy e um conjunto de testes que capturam as propriedades desejadas do modelo, e produz um modelo corrigido que passa em todos os testes. O ARepair usa testes escritos para o recentemente introduzido framework AUnit, que fornece uma noção de teste unitário para modelos de Alloy. Neste artigo, descrevemos nossa implementação em Java do ARepair, que é uma ferramenta de linha de comando, lançada como um projeto de código aberto no GitHub. Nossos resultados experimentais mostram que o ARepair é capaz de corrigir 28 dos 38 modelos defeituosos do mundo real que coletamos. O vídeo de demonstração do ARepair pode ser encontrado em https://youtu.be/436drvWvbEU.