Dafny命名規則の制御と定数の使用

Question

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

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

? global const MaxValue = 10000; ? 

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

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

Answer 1

はいとはい。

Dafnyがターゲットコードで使用するさまざまなエンティティの名前を制御するには、{:extern "ThisIsTheNameIWant"}属性を使用します。この属性は、ほとんどの宣言でサポートされています。たとえば、クラスに1つ、クラスの中に1つのメソッドを置くことができます。さらに多くの例については、DafnyテストスイートのTest/dafny0/Extern.dfyファイルを参照してください。生成されたものを見たい場合は、コマンドラインから/spillTargetCode:1フラグを使用してください。定数の

、使用：

const MaxValue := 10000 

（あなたが構築している場合は

const MaxValue: int := 10000 

を書かなければならなかったので、最近まで、あなたは、明示的定数の種類を供給しなければならなかった、注意してくださいDafnyの最新バージョンのソースから、タイプは右辺の式から推測されます）。

Ada言語から借りた素晴らしい機能は、数値リテラルの2桁。大規模なリテラルを使用して、それらの中に括弧が1つ入っている場合は、正しい番号を書いたことを目で見やすくすることができます。たとえば：

const MaxValue := 10_000 
const PhoneNumber := 512_555_1212 
const SignedInt32Limit := 0x8000_0000 

Rustan