1
내가 본 가장 강력한 사후 술어 변압기의 모든 제제는 할당 규칙을 제공한다 : 나는 궁금왜 가장 강한 사후 조건에서 실존이 필요한가? 다음과 같이
sp(X:=E, P) = ∃v. (X=E[v/X] ∧ P[v/X])
, 왜 실존 (따라서 존재 적 정량 변수 "V") 위의 필요 규칙? 가장 강한 사후 조건 술어 변환기는 상태 (변수에서 값으로의 맵핑)와 경로 조건 (프로그램의 특정 지점에서 참이어야하는 술어)을 유지한다는 점에서 기호식 평가와 거의 동일합니다. 그러나 상징적 인 평가는 실존 적 한정어에 의존하지 않습니다.
그래서 여기에 뭔가 빠져 있어야한다고 생각합니다. 어떤 도움을 주셔서 감사합니다!
내가 어떤 직관적 인 설명을 제공합니다 당신은 상징적 인 평가에 어느 정도의 지식을 가지고 있기 때문에 당신이 변수에 대한 임의의지도가있는 경우, 당신은 동안 그들을보고하기 전에 프로그램에서 미래의 상태 변경에 대해 아무것도 말할 수 없다