a [0]을 주장해야합니다.

Question

나는 현재 dafny를 배우고 있으며 정말 이상한 주장 요구 사항을 만났습니다.

method M (a : seq<int>, acc : seq<int>) 
  requires |a| > 0
  requires forall va, vacc :: va in a && vacc in acc ==> vacc <= va
{
  assert forall vacc :: vacc in acc ==> vacc <= a[0];
}

위 코드는 어설 션에서 실패하지만 추가 assert a[0] in a하면 확인합니까?

그 |a| > 0 a[0] in a이후 seq로 유지 되는 모든 상황에서 이것이 불변 인 이유 는 무엇입니까?

(또한 모든 스타일 가이드 권장 사항을 주시면 감사하겠습니다 :))

Answer 1

이것은 "트리거"와 관련이 있습니다.

짧은 대답은 수동으로 "멘션"할 때까지 a[0]Dafny가 수량화 된 requires절 을 이용할 수 없다는 것 입니다. 당신이 그것을 어떻게 언급 하든 상관 없습니다 a[0]. 그것이 논리적으로 아무것도 추가하지 않는 것처럼 보이지만 사소한 주장이 작동하는 이유 a[0]입니다.

자세한 내용은 다음을 참조하십시오.

• 자주 묻는 질문 qustion
• 이 대답은 "트리거가 무엇입니까?"
• "트리거 할 용어를 찾을 수 없음"에 대한 이 답변