잠시 동안 검색했지만 "predicate checking"에 대한 간결한 정의를 찾을 수 없습니다. 언제 술어 검사를 적용 할 수 있습니까? 호아의 트리플과 비교하면 어떨까요? Hoare의 트리플을 모든 코드 행에 올바르게 적용하면 소프트웨어의 정확성을 보장 할 수 있다고 생각합니다. (내가 틀렸다면 나를 바로 잡아주세요.) 술어 검사가 동일한 속성을 가질 수 있습니까? 질문 자체가 잘못 구성된 경우 사과드립니다. 나는 정말로 술어 검사가 무엇을하는지 모른다.술어 검사 란 무엇입니까?
술어은 참 또는 거짓 결과와 동일한 논리 문장 또는 기능입니다.
절차 적 언어 및 선언적 언어 모두에서 술어의 가장 간단한 예는 guard 절과 assertion입니다.
> if (x != null) then ...
> assert x != null
Hoare의 사전 조건 및 사후 조건은 술어의 예입니다. 나는 Hoare에 캡슐화 된 명령문의 세분성에 대해 명시적인 사항이 없다고 생각합니다. 단, post-condition으로의 단일 이탈 경로가 있어야합니다. 단일 명령문, 함수 또는 전체 프로세스 일 수 있습니다.
불변 식은 술어의 특수한 경우이며 사후 조건 = 사전 조건입니다.
아마도 가장 순수한 예가 프롤로그입니다. 모든 문은 술어입니다. 또 다른 예는 에펠 (Eiffel)에서 사용되는 계약 별 설계 (design-by-contract)이며, LISP의 빈 목록은 또한 술어입니다.
"소프트웨어의 정확성 보장"에 동의하기를 꺼려하고 정확성이 조건부에 부합 함을 증명하지 못합니다.
업데이트