我想开发一个用于Dafny的多线程库，但遇到了像这样的问题：

我有这个Dafny程序（作为基础版本）：

datatype ThreadState = Dead | Running | Paused
method {:extern} SleepInMilliseconds(milliseconds : nat)
method WaitFor(thread: Thread)
class Thread {
  var state : ThreadState
  var phases: ThreadPhase

  method GetState() returns (state : ThreadState)
    ensures state == this.state
  {
    return this.state;
  }
  method SetState(newState: ThreadState)
    ensures newState == state
    requires if state == Dead then newState != Paused else true
    modifies `state
  {
    state := newState;
  }
  method runThreadExecutableParts(instance: ThreadPhase)
    decreases *
    requires !(instance.ThreadLoop?)
  {
    match instance
    case ThreadExecutablePart(ranFunction,next) => {
      run(ranFunction);
      runThreadPhases(instance.next);
    }
    case End => return;
  }

  method runThreadLoop(instance : ThreadPhase)
    requires instance.ThreadLoop?
    decreases * {
    var head := instance.content;
    var currentThreadPhase := head;
    while !(instance.escapeCondition())
      decreases * {
      currentThreadPhase := if currentThreadPhase.End? then head else currentThreadPhase.next;
      runThreadPhases(currentThreadPhase);
    }
    runThreadPhases(instance.next);
  }
  /** 
  Runs thread phases by calling the right methods to run either ThreadLoops or ThreadThreadExecutableParts
  */
  method runThreadPhases(instance : ThreadPhase)
    decreases * {
    if instance.ThreadLoop? {
      runThreadLoop(instance);
    } else {
      runThreadPhases(instance);
    }
  }
  method run(t : Runnable)
}

class Runnable {

}
/**
A stopable chunk of code (phase) that can form other phases
 */
datatype ThreadPhase =
  /** Means that there's no more phases to read */
  | End
  /** A part which gets executed via an external Java library */
  | ThreadExecutablePart(ranFunction: Runnable, next : ThreadPhase)
  /** A while loop which contains other ThreadPhases and which ends if a call to its escapeCondition function parameter returns true */
  | ThreadLoop(content: ThreadPhase, escapeCondition: () ~> bool, next : ThreadPhase)

在包含 while !(instance.escapeCondition()) 语句的那一行，验证器会抱怨函数 escapeCondition() 的前置条件未被满足，尽管我甚至还没有设置一个前置条件！

escapeCondition 是一个不接受任何参数、返回布尔值的函数，而且这个布尔值仅基于它的reads子句中的值。由于它的实现可能因API用户而异，我不想限制这个函数的 reads 子句。

我应该如何解决这个问题？

解决方案

已修复。问题只是出在使用一个包装器。

type Runnable = Function<(),()>
type Predicate = Supplier<bool>
type Supplier<OutType> = Function<(),OutType>
type Consumer<InType> = Function<InType,()>
trait Function<InType,OutType> {
  method runWith(input : InType) returns (output : OutType)
}