타입에 값의 조건 더하기
정수 타입은 값의 표현 형식을 알려 주지만 그 값이 특정 범위 안에 있는지까지 항상 나타내지는 않는다. Flux는 타입에 논리 제약을 붙여 허용하는 값의 집합을 더 좁게 표현한다. 동명의 GitOps 도구와는 별개이며 Rust 프로그램의 정확성 조건을 정적으로 다루는 도구다.
입력과 출력의 관계
함수가 받는 값의 조건과 반환할 값의 성질을 함께 기술할 수 있다. 반환값이 특정 조건을 만족한다는 요구와 입력에 따라 정확한 값을 반환한다는 요구는 강도가 다르다. 필요한 관계를 충분히 표현해야 검증 성공이 실제 요구에 대응한다. 호출 지점에서도 전제조건이 성립하는지 확인한다.
명세와 확인 범위
조건에는 효율적으로 판정할 수 있는 논리 표현의 부분집합을 사용하며 임의의 Rust 코드를 그대로 논리식으로 사용하는 방식은 아니다. 작성한 계약에서 빠진 성질은 자동으로 추가되지 않는다. 검증에 맞춘 가정이 실제 사용 조건과 일치하는지 확인하고 대상 코드와 도구의 지원 범위를 함께 관리한다.