key
KeY-2.12.2 (2023-11-10)
Este repositório é o lar do teorema interativo Chave para verificação e análise formal dos programas Java. A chave vem como um aplicativo independente da GUI, que permite verificar a correção funcional dos programas Java em relação às especificações formais formuladas no JAVA Modeling Language JML. Além disso, a chave também pode ser usada como uma biblioteca, por exemplo, para execução simbólica do programa, raciocínio de primeira ordem ou geração de casos de teste.
Para mais informações, consulte
java.util.IdentityHashMap ,LinkedListA versão atual da chave é 2.12.2, licenciada no GPL V2.
Sinta -se à vontade para usar os modelos de projeto para começar a usar a chave:
Esta pasta fornece um projeto gerenciado por gradle após o layout da pasta padrão do Maven. Existem vários subprojetos nesta pasta. Em geral, todas key.*/ Subproject contém um componente principal da chave. Componentes adicionais e opcionais estão no keyext.*/ Pastas. O arquivo build.gradle é o script de construção root que descreve as dependências e tarefas de construção comuns para todos os subprojetos.
key.util , key.core e key.ui são a base para o produto "Provedor -chave". É necessário um cuidado especial se você planeja fazer alterações aqui.
Supondo que você esteja no diretório deste arquivo ReadMe, você pode criar uma versão executável e implantável com um desses comandos:
Com ./gradlew key.ui:run você pode executar a interface do usuário diretamente do repositório. Use ./gradlew key.ui:run --args='--experimental' para ativar recursos experimentais.
Use ./gradlew classes para compilar a chave, que inclui a execução de Javacc e Antlr. Da mesma forma, use ./gradlew testClasses se você também deseja compilar as classes de teste JUNIT.
Teste sua instalação com ./gradlew test . Esteja ciente de que isso geralmente leva várias horas para ser concluído. Com ./gradlew testFast , você pode executar uma suíte de teste mais leve que deve ser concluída em alguns minutos.
Você pode selecionar um caso de teste específico com o argumento --tests . Os curingas são permitidos.
./gradlew :key. < subproject > :test --tests " <class>.<method> " Você pode depurar a chave adicionando a opção --debug-jvm e, em seguida, anexando um depurador no localhost:5005 .
Você pode criar uma única versão de jar, também conhecida
./gradlew :key.ui:shadowJar O arquivo é gerado em key.ui/build/libs/key-*-exe.jar .
Uma distribuição é construída com
./gradlew :key.ui:installDist :key.ui:distZip A distribuição pode ser testada chamando key.ui/install/key/bin/key.ui e é fechado em key.ui/build/distributions .
A distribuição fornece potencial para usar arquivos de jar único.
A qualidade é avaliada automaticamente usando o Sonarqube em cada solicitação de tração. Os resultados das avaliações (aprovação/falha) podem ser inspecionados na seção de cheques do PR.
As regras e o portão de qualidade são mantidas por Alexander Weigl [email protected] atualmente.
Mais diretrizes e documentação para o desenvolvimento principal podem ser encontradas em doces-chave.
Para relatórios de bug, use o rastreador de problemas ou envie um e-mail para [email protected].
Para discussões, convém se inscrever e usar a lista de discussão key-llis.lists.informatik.kit.edu ou usar discussões no github.
Sinta -se à vontade para enviar solicitações de tração via github. As solicitações de tração são avaliadas usando testes automáticos, formatação e damas de origem estática, bem como uma revisão manual de um dos desenvolvedores. Mais diretrizes e documentação para o desenvolvimento principal podem ser encontradas em doces-chave.
This is the KeY project - Integrated Deductive Software Design
Copyright (C) 2001-2011 Universität Karlsruhe, Germany
Universität Koblenz-Landau, Germany
and Chalmers University of Technology, Sweden
Copyright (C) 2011-2024 Karlsruhe Institute of Technology, Germany
Technical University Darmstadt, Germany
Chalmers University of Technology, Sweden
The KeY system is protected by the GNU General Public License.
See LICENSE.TXT for details.
