key 다운로드 - key 소스 코드 다운로드

key

기타 카테고리

KeY-2.12.2 (2023-11-10)

다운로드

키 - 연역적 Java 프로그램 검증 자

이 저장소는 Java 프로그램의 공식적인 검증 및 분석을위한 대화식 Theorem Prover 키의 홈입니다. Key는 독립형 GUI 응용 프로그램으로 제공되므로 Java 모델링 언어 JML에 공식화 된 공식 사양과 관련하여 Java 프로그램의 기능적 정확성을 확인할 수 있습니다. 또한, 키는 또한 상징 프로그램 실행, 1 차 순서 추론 또는 테스트 사례 생성을위한 라이브러리로 사용될 수 있습니다.

자세한 내용은 참조하십시오

주요 홈페이지
키 북
주요 개발자 문서
키의 성공 사례 :
- JDK 분류 루틴 (Timsort)에서 발견 된 심각한 버그,
- java.util.IdentityHashMap 의 확인,
- LinkedList 의 버그 분석에 대한 Google 상

Key의 현재 버전은 2.12.2이며 GPL V2에 따라 라이센스가 부여됩니다.

프로젝트 템플릿을 사용하여 키를 사용하여 시작하십시오.

검증 프로젝트
도서관으로 사용합니다
상징적 실행 백엔드로 사용합니다

요구 사항

하드웨어 :> = 2GB RAM
운영 체제 : Linux/Unix, MacOSX, Windows
Java 17 이상
선택적으로 키는 다음 바이너리를 사용할 수 있습니다.
- SMT 솔버 :
  - Z3
  - CVC5
  - CVC4
  - 공주

키 폴더의 내용

이 폴더는 Maven의 표준 폴더 레이아웃에 따라 Gradle 관리 프로젝트를 제공합니다. 이 폴더에는 여러 하위 프로젝트가 있습니다. 일반적으로 모든 key.*/ 하위 프로젝트에는 키의 핵심 구성 요소가 포함되어 있습니다. 추가 및 선택적 구성 요소는 keyext.*/ 폴더에 있습니다. File build.gradle 모든 하위 프로젝트의 종속성 및 공통 빌드 작업을 설명하는 루트 빌드 스크립트입니다.

key.util , key.core 및 key.ui 는 제품 "Key Prover"의 기반입니다. 여기에서 변경하려는 경우 특별한주의가 필요합니다.

키를 컴파일하고 실행하십시오

이 readme 파일의 디렉토리에 있다고 가정하면 이러한 명령 중 하나를 사용하여 실행 가능하고 배포 가능한 버전을 만들 수 있습니다.

./gradlew key.ui:run 리포지토리에서 직접 키의 사용자 인터페이스를 실행할 수 있습니다. ./gradlew key.ui:run --args='--experimental' 사용하여 실험 기능을 활성화하십시오.
Javacc 및 Antlr 실행을 포함하여 ./gradlew classes 컴파일하는 키를 사용하십시오. 마찬가지로 Junit 테스트 클래스를 컴파일하려면 ./gradlew testClasses 사용하십시오.
./gradlew test 로 설치를 테스트하십시오. 이것은 일반적으로 완료하는 데 몇 시간이 걸릴 것입니다. ./gradlew testFast 사용하면 몇 분 안에 완료 해야하는보다 경량 테스트 스위트를 실행할 수 있습니다.
--tests 인수로 특정 테스트 사례를 선택할 수 있습니다. 와일드 카드가 허용됩니다.
```
./gradlew :key. < subproject > :test --tests " <class>.<method> "
```
--debug-jvm 옵션을 추가 한 다음 localhost:5005 에 디버거를 첨부하여 키를 디버그 할 수 있습니다.
Key의 단일 항아리 버전, 일명 Fat Jar를 만들 수 있습니다.
```
./gradlew :key.ui:shadowJar
```
파일은 key.ui/build/libs/key-*-exe.jar 에서 생성됩니다.
분포가 빌드됩니다
```
./gradlew :key.ui:installDist :key.ui:distZip
```
분포는 key.ui/install/key/bin/key.ui 호출하여 테스트 할 수 있으며 key.ui/build/distributions 에 ZIPTED를받습니다.
배포는 단일 JAR 파일을 사용할 가능성을 제공합니다.

키 개발

각 풀 요청에서 Sonarqube를 사용하여 품질이 자동으로 평가됩니다. 평가 결과 (Pass/Fail)는 PR의 점검 섹션에서 검사 할 수 있습니다.
규칙과 품질 게이트는 현재 Alexander Weigl [email protected]에 의해 유지됩니다.
주요 개발에 대한 더 많은 지침 및 문서는 Key-DOC에서 찾을 수 있습니다.

문제 및 버그 보고서

버그 보고서는 문제 추적기를 사용하거나 [email protected]로 메일을 보내십시오.
토론을 위해서는 메일 링리스트 [email protected]를 구독하고 사용하거나 GitHub 토론을 사용하십시오.

키에 기여합니다

Github를 통해 풀 요청을 제출하십시오. 풀 요청은 자동 테스트, 서식 및 정적 소스 검사기와 개발자 중 한 사람의 수동 검토를 사용하여 평가됩니다. 주요 개발에 대한 더 많은 지침과 문서는 Key-DOC에서 찾을 수 있습니다.

라이센스 비고

 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.

확장하다

추가 정보