构造函数的数据类型和顺序

Question

以下定义有区别吗？

datatype Nat = S(Nat) | Z

和

datatype Nat = Z | S(Nat)

我预计不会，但有趣的是，以下代码在第一个定义中编译良好，但在第二个定义中编译不正确。

function natToDay(n : Nat) : Day
  decreases n
{
  match n {
    case Z                      => Monday
    case S(Z)                   => Tuesday
    case S(S(Z))                => Wednesday
    case S(S(S(Z)))             => Thursday
    case S(S(S(S(Z))))          => Friday
    case S(S(S(S(S(Z)))))       => Saturday
    case S(S(S(S(S(S(Z))))))    => Sunday
    case S(S(S(S(S(S(S(k))))))) => natToDay(k)
  }
}

lemma {:induction n} proof(n : Nat)
  ensures natToDay(n) == Sunday    ==> natToDay(n) == Sunday
  ensures natToDay(n) == Saturday  ==> natToDay(S(n)) == Sunday
  ensures natToDay(n) == Friday    ==> natToDay(S(S(n))) == Sunday
  ensures natToDay(n) == Thursday  ==> natToDay(S(S(S(n)))) == Sunday
  ensures natToDay(n) == Wednesday ==> natToDay(S(S(S(S(n))))) == Sunday
  ensures natToDay(n) == Tuesday   ==> natToDay(S(S(S(S(S(n)))))) == Sunday
  ensures natToDay(n) == Monday    ==> natToDay(S(S(S(S(S(S(n))))))) == Sunday
{}

第一个数据类型定义产生：

Dafny program verifier finished with 2 verified, 0 errors
Wrote textual form of target program to test.cs

第二个产生：

/Users/boro/Desktop/dafny/test.dfy(27,0): Error: A postcondition might not hold on this return path.
/Users/boro/Desktop/dafny/test.dfy(21,54): Related location: This is the postcondition that might not hold.
Execution trace:
...

Answer 1

两者之间应该没有任何区别。请在 https://github.com/dafny-lang/dafny/issues.

上报告此问题

构造函数的数据类型和顺序

Datatypes and order of constructors

dafny