Dafny中如何避免int/real等全序类型的代码重复？

针对你遇到的int、real这类全序类型无法复用中位数逻辑的问题，有两种可行的解决方式：

方法1：用Trait模拟类型类 + 隐式参数 #

Dafny没有直接的泛型约束语法，但可以通过trait定义全序接口，再为目标类型实现该接口，结合隐式参数自动推导实现，从而复用核心逻辑。

1. 定义全序trait，封装比较操作：

trait TotalOrder<T> {
  function Leq(a: T, b: T): bool
  function Lt(a: T, b: T): bool {
    Leq(a, b) && !Leq(b, a)
  }
}

2. 为int和real分别实现这个trait，并定义隐式实例让Dafny自动识别：

module IntOrder {
  export trait TotalOrder<int> {
    function Leq(a: int, b: int): bool {
      a <= b
    }
  }
  implicit function Instance(): TotalOrder<int> {
    new TotalOrder<int> {}
  }
}

module RealOrder {
  export trait TotalOrder<real> {
    function Leq(a: real, b: real): bool {
      a <= b
    }
  }
  implicit function Instance(): TotalOrder<real> {
    new TotalOrder<real> {}
  }
}

3. 编写泛型中位数函数，依赖TotalOrder的隐式参数：

function Median<T>(s: seq<T>) (order: TotalOrder<T>): T
  requires s != []
{
  let sorted := Sort(s, order)
  sorted[s.Length / 2]
}

// 通用排序辅助函数，基于传入的全序规则
function Sort<T>(s: seq<T>, order: TotalOrder<T>): seq<T> {
  if s.Length <= 1 then s else
    let pivot := s[0],
        less := [x | x in s[1..] :: order.Leq(x, pivot)],
        greater := [x | x in s[1..] :: order.Lt(pivot, x)]
    Sort(less, order) + [pivot] + Sort(greater, order)
}

4. 调用时无需手动传递排序规则，Dafny会自动匹配对应的隐式实例：

method Main() {
  let intSeq := [3,1,2]
  let realSeq := [3.5, 1.2, 2.7]
  print Median(intSeq); // 自动使用IntOrder的实现
  print Median(realSeq); // 自动使用RealOrder的实现
}

方法2：多态重载 + 共享核心逻辑 #

如果不想用trait和隐式参数，可以把核心逻辑抽成通用辅助函数，再为int、real分别写外层的重载函数，只做类型适配：

// 通用中位数核心逻辑，接受自定义比较函数
function MedianCore<T>(s: seq<T>, leq: (T, T) -> bool): T
  requires s != []
{
  let sorted := SortCore(s, leq)
  sorted[s.Length / 2]
}

// 通用排序核心逻辑
function SortCore<T>(s: seq<T>, leq: (T, T) -> bool): seq<T> {
  if s.Length <= 1 then s else
    let pivot := s[0],
        less := [x | x in s[1..] :: leq(x, pivot)],
        greater := [x | x in s[1..] :: !leq(pivot, x)]
    SortCore(less, leq) + [pivot] + SortCore(greater, leq)
}

// 针对int的中位数函数
function MedianInt(s: seq<int>): int
  requires s != []
{
  MedianCore(s, (a, b) => a <= b)
}

// 针对real的中位数函数
function MedianReal(s: seq<real>): real
  requires s != []
{
  MedianCore(s, (a, b) => a <= b)
}

这种方式虽然仍需写外层的类型专属函数，但核心逻辑只维护一次，大幅减少重复代码。

补充说明 #

对于ORDINAL类型，完全可以套用方法1的模式，实现TotalOrder<ORDINAL>的trait和隐式实例，直接复用同一个Median函数。

内容的提问来源于stack exchange，提问作者Frank Seidl