Why3 é uma plataforma de verificação de programas e sistemas formais. Ele fornece uma linguagem de especificação, chamada de WhyML, que permite descrever formalmente o comportamento de programas. A principal finalidade do Why3 é facilitar a verificação formal, ou seja, garantir matematicamente que um programa atende a determinadas propriedades específicas.

Algumas das principais funcionalidades e usos do Why3 incluem:

  1. Especificação Formal: Permite aos desenvolvedores especificar formalmente o comportamento desejado de um programa. Isso é feito usando a linguagem WhyML.
  2. Geração de Condições de Prova: O Why3 é capaz de gerar automaticamente condições de prova a partir das especificações fornecidas. Isso é essencial para verificar se o código implementa corretamente as propriedades especificadas.
  3. Integração com Provers Automáticos e Interativos: O Why3 suporta uma variedade de provers automáticos e interativos, como o Z3, Alt-Ergo e outros. Isso permite a automação do processo de verificação formal.
  4. Verificação de Programas em Diversas Linguagens: Embora a linguagem de especificação seja WhyML, o Why3 pode ser usado para verificar programas escritos em várias linguagens de programação, incluindo C, Java e Ada.
  5. Desenvolvimento de Sistemas Críticos: O Why3 é particularmente útil em ambientes onde a correção do software é crítica, como em sistemas embarcados, sistemas de controle, e em outros contextos nos quais falhas podem ter consequências graves.
  6. Ensino e Pesquisa em Verificação Formal: O Why3 é usado em ambientes acadêmicos para ensinar e realizar pesquisas em verificação formal de software.

Em resumo, o Why3 é uma ferramenta poderosa para a verificação formal de programas, proporcionando uma abordagem sistemática e matematicamente fundamentada para garantir a corretude do software.

1. Declaração de Tipos:

2. Declaração de Funções:

3. Estruturas Condicionais: