This paper presents a strategy for oracle generation for software testing from formal specification that aims increase the aplicability of the oracle generators. By this estrategy is possible generate oracles for implementations that are not generated directy from the formal specification strucutre and that can be applied to any test case generation technique. The estrategy is the base to OZJ tool which automates part of the oracle generate process for class Java from Object-Z specifications.

Este artigo apresenta uma estratégia para geração de oráculos para teste de software a partir de especificação formal que visa aumentar a abrangência da aplicabilidade dos geradores de oráculo. A estratégia permite gerar oráculos para implementações não derivadas diretamente da estrutura da especificação e que podem ser aplicados a casos de testes derivados de qualquer técnica de seleção de casos de teste. A estratégia apresentada é a base para a implementação da ferramenta OZJ, a qual automatiza parte do processo de geração do oráculo para classes Java a partir de especificações Object-Z.