0

Dafny がターゲット コードに使用する命名規則を制御する方法はありますか?

シンボリック定数をグローバルに使用することは可能ですか? このようなもの：

? global const MaxValue = 10000; ?

method Method1 (a : int) returns (b : int)
  requires a < MaxValue

数値式を文字列に変換する方法はありますか?

4

1 に答える 1