Dafny에서 기본형 작성

기본형

꽤 자주 Dafny에게 다양한 수학적 사실을 설명해야 합니다. 이를 수행하는 방법은 기본적으로 고스트 메서드인 기본형을 작성하는 것입니다. 다른 함수나 메서드와 마찬가지로 입력 매개변수, 반환 값, 사전 조건 및 사후 조건을 가질 수 있습니다. 그러나 기본형은 사양 컨텍스트에만 존재하며 실행 가능한 코드로 컴파일되지 않습니다.

기본형 작성 가이드here가 있습니다.

직접 증명: 관계에 대한 예

ARelation는 다른 집합의 개체의 순서 쌍 집합입니다. 가장 일반적인 예는 작거나 같음과 같은 정수 순서 관계입니다. 정수 1-3으로 제한하면 it을 이렇게 인코딩할 수 있습니다.

var lessThanEqual := {
(1,1),
(1,2),
(1,3),
(2,2),
(2,3),
(3,3)
};

쌍 (1,3)이 lessThanEqual 집합에 있으면 1이 3보다 작거나 같다고 말할 수 있습니다.

많은 유형의 관계가 있습니다. 술어 함수를 사용하여 Dafny에서 이러한 유형을 정의할 수 있습니다. 입력 유형을 유형 변수 T로 매개변수화하여 일반 함수를 만들 수 있습니다.

predicate relationOnASet<T>(R: set<(T,T)>, S: set<T>) {
    forall ts :: ts in R ==> ts.0 in S && ts.1 in S
}

predicate reflexive<T>(R: set<(T,T)>, S: set<T>) 
    requires relationOnASet(R, S)
{
    forall s :: s in S ==> (s,s) in R
}

predicate symmetric<T>(R: set<(T,T)>, S: set<T>)
    requires relationOnASet(R, S)
{
    forall x: T, y:T :: x in S && y in S && (x,y) in R ==> (y, x) in R
}

predicate transitive<T>(R: set<(T,T)>, S: set<T>) 
    requires relationOnASet(R, S)
{
    forall a,b,c :: a in S && b in S && c in S && (a,b) in R && (b,c) in R ==> (a,c) in R
}

predicate equivalenceRelation<T>(R: set<(T,T)>, S: set<T>) 
    requires relationOnASet(R, S)
{
    reflexive(R, S) && symmetric(R, S) && transitive(R, S)
}

관계의 연합?

관계는 집합일 뿐이고 집합 합집합을 사용하여 집합을 결합할 수 있으므로 특정 종류의 관계 합집합에 대해 무엇을 말할 수 있습니까? Dafny는 세트로 작업할 때 +를 오버로드하여 세트 합집합을 의미합니다.

두 개의 대칭 관계를 합집합해도 결과는 여전히 대칭입니까? 우리는 Dafny에서 이렇게 증명할 수 있습니다.

lemma symmetricUnion<T>(R_1: set<(T,T)>, S_1: set<T>, R_2: set<(T,T)>, S_2: set<T>)
    requires |R_1| > 0
    requires |R_2| > 0
    requires |S_1| > 0
    requires |S_2| > 0
    requires relationOnASet(R_1, S_1)
    requires relationOnASet(R_2, S_2)
    requires symmetric(R_1, S_1)
    requires symmetric(R_2, S_2)
    ensures symmetric(R_1+R_2, S_1+S_2)
{
    forall x,y | x in S_1+S_2 && y in S_1+S_2 && (x,y) in R_1+R_2
        ensures (y,x) in R_1+R_2
    {
        if  x in S_1 && y in S_1 && (x,y) in R_1 {
            assert (y,x) in R_1+R_2;
        }else if  x in S_2 && y in S_2 && (x,y) in R_2 {
            assert (y,x) in R_1+R_2;
        }
    }
}

그러나 전이 관계에 대해 동일한 질문을 하면 문제에 봉착합니다. 반례를 만들 수 있습니다.

lemma transitiveUnionCounterExample<T>()
  returns (
  R1: set<(T, T)>, S1: set<T>,
  R2: set<(T, T)>, S2: set<T>)
  ensures relationOnASet(R1, S1)
  ensures relationOnASet(R2, S2)
  ensures transitive(R1, S1)
  ensures transitive(R2, S2)
  ensures ! transitive(R1 + R2, S1 + S2)
{
  var a : T :| assume true;
  var b : T :| assume a != b;
  var c : T :| assume a != c && b != c;
  S1 := {a, b};
  S2 := {b, c};
  R1 := {(a, b)};
  R2 := {(b, c)};
}

lemma transitiveUnionNotAlwaysTransitive<T>()
  ensures !
  (forall S1 : set<T>, S2 : set<T>, R1 : set<(T,T)>, R2 : set<(T, T)> ::
  relationOnASet(R1, S1) &&
  relationOnASet(R2, S2) &&
  transitive(R1, S1) &&
  transitive(R2, S2)  ==> transitive(R1 + R2, S1 + S2)
  )
{
  var a, b, c, d := transitiveUnionCounterExample<T>();
}

Dafny의 모순에 의한 증명

Dafny의 작성자는 모순에 의한 증명을 위해 다음 템플릿을 권장합니다.

lemma L(...)
  requires P
  ensures Q
{
  if !Q {
    ...
    assert !P;
    assert false;
  }
}

여기서 목표는 우리가 어떤 명제에 대해 !Q를 가정하면 일부 계산이나 단언을 통해 !P를 암시한다는 것을 보여줄 수 있으며 이는 필수 전제 조건에 의해 참이라고 가정되면 모순에 도달한 것입니다.

false를 주장하는 것은 이 분기가 모순으로 끝날 것으로 예상한다는 것을 분명히 하는 추가 단계입니다.