평등 합금

Question

에서 나는 다음과 같은 포함하는 합금 모델있어?

Answer 1

당신의 질문에서 당신이하고 싶은 것이 명확하지 않다. 샘플 합금 코드에서 혼란을 겪고있는 것처럼 보인다.

첫 번째로 표시 할 모델은 두 가지 다른 방법으로 성별 이름을 사용합니다. 이는 불법이 아니지만 혼란을 유발하는 것으로 보입니다.

두 개의 싱글 톤 서명 john과 Steve에 대한 성명에서 젠더는 두 개의 이진 관계를 나타냅니다. 하나는 서명 john과 서명자 사이에 있고, 다른 하나는 스티브 (Steve) 사이에 있습니다. 그리고 남자. 젠더는 상징적 형태로 똑같은 것을 말하면서, (a) 존 -> 사람의 일부 집합과 (b) 스티브 -> 사람의 일부 집합을 나타냅니다.

그러나 익명의 사실에서 성별은 man 유형의 변수를 나타냅니다.

모델 중 하나의 이름을 바꾸거나 다른 이름을 바꿀 수있는 방법을 찾으면 모델을보다 쉽게 ​​이해할 수 있습니다. 정량화 식의 변수 이름이 임의이기 때문에, 당신의 사실은 당신이 말을 다음 말을 의미가 있습니다 의미 한 무슨을하지 않으면 당신은

fact { all P : person, M : man | P.M = P.M => person = person } 

로 재구성하면 같은 일을 의미합니다 뭔가

같은

fact { all P : person, M : man | 
    P.Gender = P.Gender => person = person 
} 

변수의 이름을 변경하면 하나의 의미 또는 다른 것을 선택해야합니다. 이것은 좋은 일입니다. (. 그것은 어느 제제는 합금에 실제로 만족하지만 이제 한 번에 하나의 문제를 해결 할 수 있다는 불행한 사실은, 이름 성별의 이중 사용을 치우는 것이 첫 번째 단계입니다.)

두 번째 문제 당신이 의미하는 사실의 공식화가 무엇이든 그것이 당신이 의미하고자하는 것을 거의 의미하지는 않습니다. 표현이 V1.V2 또는 V1.Relation 중입니다 잠시 모델의 세부 사항을 무시하여 사실은 모델에서 정의 된 일부 관계에 대한 양식을

fact { all V1 : sig1, V2 : sig2 | 
    Expression = Expression => sig1 = sig1 
} 

걸립니다. 몇 가지 잘못된 여기에 있습니다 : 도트 연산자는 인수 중 하나의 이름 인 경우에만 의미가 있습니다 : V1 및 V2가 주어진 서명에 이르기 서명 또는 변수의 두 이름이있는 곳

• V1.V2 의미가 관계.

• 식 E가 전혀 의미가 없으면 E = E 형식의 부울 식 (예 : person.Gender = person.Gender)은 E의 의미와 관계없이 true입니다. E로 표시된 것은 자연적으로 그 자체와 동일 할 것입니다. 그래서 조건뿐만 아니라 같은 이유로

  1 = 1 => person = person 
  

• 을 기록 할 수있는, 사람 = 사람에 관계없이 항상 모델의 사실이 될 것이다 : 어떤 모델 인스턴스의 인스턴스 사람의 집합은 동일합니다 인스턴스에있는 사람의 집합. 따라서 조건부는 항상 true 일 것이고 사실은 모델의 인스턴스에 실제로 제약을 가하지 않을 것입니다.

앞으로 나아갈 수있는 방법이 명확하지 않습니다. 아마 시작하는 한 가지 방법은 자신이 모델에서 포착하려고하는 다음 진술 중 어느 것을 스스로에게 물어 보는 것입니다.

• 사람이 있습니다.
• 일부 사람은 남성입니다 (성별 = '남자'). 다른 사람들은 남성이 아닙니다.
• 존은 남성 개인입니다.
• 스티브는 남성입니다.
• 존과 스티브는 뚜렷한 개인입니다.
• x와 y가 동일한 성별을 가진 개인 인 경우 x와 y는 동일한 개체입니다. 나는. 두 명의 개인이 같은 성별을 갖고 있지 않습니다.

이러한 진술은 모두 동시에 사실 일 수는 없습니다. (분명하지 않은 경우 이유를 알아 내려고 시도하는 것보다 나빠질 수 있습니다. 합금이 도움이 될 수 있습니다.)

행운을 빈다.