아래는 이메일 주소록의 Alloy 모델입니다. 주소록의 각 이름은 이름 또는 주소에 매핑됩니다.
결국 각 이름이 주소 (예 : Family-> Tom-> Tom_addr)에 매핑되기를 원합니다. 나는 이것을 구현하기 위해 사실을 만들었습니다. 내 사실이 정확한지 확인하기 위해 어설 션을 만들었습니다.
나는 주장에 무엇을 넣을지 오랫동안 의아해했다. 이상하게도 "fact"섹션에 배치 한 표현이 assert에 배치하기에 적합한 표현 인 것 같습니다. 그러나 그 주장은 단지 사실을 반복하는 것일뿐 도움이되지 않습니다. 그래서 저는 주장 할 다른 것을 만들었습니다.
"assert"섹션에 배치 한 내용이 실제로 모든 이름이 결국 주소에 매핑되는지 확인한다고 전적으로 확신하지는 않습니다.
질문 :
"사실"섹션에서 각 이름이 결국 주소에 매핑되는 제약 조건을 올바르게 표현 했습니까?
"assert"섹션에서 모든 이름이 결국 주소에 매핑되도록하는 더 좋은 방법이 있습니까?
sig Addr {}
sig Name {
address: some Addr + Name
}
fact {
// No cycles.
no n: Name | n in n.^address
// All names eventually map to an Addr.
// Here's how I implemented the constraint:
// There is no name n that is mapped-to (i.e., m -> n),
// which does not map-to something (i.e., n -> p).
no n: Name {
n in univ.address
n not in address.univ
}
}
assert All_names_eventually_map_to_an_Addr {
all n: Name | some n.^address & Addr
}
check All_names_eventually_map_to_an_Addr
사실을 반복하는 주장은 실제로 유용하기 때문에 원하지 않는 것입니다. (가정 하에서 속성을 확인 / 증명하는 것을 생각해보십시오. (Q 및 P) 형식의 의미는 P 가 모든 P 및 Q에 대해 명확하게 유지됨을 의미 합니다.)
즉, 속성 :
모든 이름은 결국 주소에 매핑됩니다.
코드 스 니펫에 제공된대로 올바르게 표현되어야합니다. (의 인스턴스에 대해 Address관계 address가 정의되지 않았으므로 클로저는의 한 요소에만 매핑 할 수 있습니다 Address.)
이 기사는 인터넷에서 수집됩니다. 재 인쇄 할 때 출처를 알려주십시오.
침해가 발생한 경우 연락 주시기 바랍니다[email protected] 삭제
몇 마디 만하겠습니다