达夫尼序列何时相等？

编程问答 2022-06-13

问题描述

嗨，已经定义了一个从集合中构建序列的函数，可以很容易地验证从相等集合中该函数必须返回相等的序列。但这不是结果看起来很像

qr = [3,1,2] ==  qt = [1,2,3]  ??

我正在使用VScode并运行所谓的Dafny 0.18.0。达夫妮（Dafny）中的错误或对我的误解。
欢迎任何更正。

predicate setIsSeq<T>(t : set<T>,q : seq<T>) 
{ (|t| == |q|)  ==>
   (forall i :: (0 <= i < |q|) ==> (q[i] in t)) &&
   (forall x :: x in t ==> (x in q))
}
function method fSetToSeq<T>(t : set<T>) : (r : seq<T>)
  decreases t 
  ensures setIsSeq(t,r);
 {
  var inner := t; 
  if (|inner| == 0) then [] 
  else (
    var e :| e in inner; 
    var tx := inner - {e};
    var qx := fSetToSeq(tx);
    [e] + qx   )
  }   
  lemma {:induction s1,s2} whatIsSeq<T>(s1 : set<T>,s2 : set<T>)     
  ensures  s1 == s2 ==> fSetToSeq(s1) == fSetToSeq(s2)  {}

method Main() {
var st:set<nat> := {1,3};
var sr:set<nat> := {3,2};
assert st == sr;
var qr:seq<nat> := fSetToSeq(sr);
var qt:seq<nat> := fSetToSeq(st);
assert qr == qt;
print "qr = ",qr," ==  qt = ",qt,"  ??  \n";

var xr:seq<nat> := [1,3];
var yr:seq<nat> := [3,2];
print "yr = ",yr," !=  xr = ",xr,"  ??  \n";
assert yr != xr;
}

解决方法

是的，绝对是一个错误。这与this question中的错误相同。 fSetToSeq不应被编译。请报告github。

dafnyequalitysequencesequencesequence