控制Dafny命名約定和使用常量

Question

有什麼辦法來控制Dafny用於目標代碼的命名約定？

是否可以在全局範圍內使用符號常量？這樣的事情：

? global const MaxValue = 10000; ? 

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

有什麼辦法將數值表達式轉換爲字符串？

Answer 1

是的，是的。

要控制Dafny在目標代碼中使用的各種實體的名稱，請使用{:extern "ThisIsTheNameIWant"}屬性。大多數聲明都支持該屬性。例如，您可以將一個放在類上，另一個放在類中的方法上。有關更多示例，請參閱Dafny測試套件中的Test/dafny0/Extern.dfy文件。如果您想查看生成的內容，請使用命令行中的/spillTargetCode:1標誌。

常量，使用：

const MaxValue := 10000 

（注意，直到最近，你必須明確提供的常量類型，所以你必須寫

const MaxValue: int := 10000 

如果你正在構建的最新版本的Dafny來源，類型可以從右邊的表達式中推斷出來）

從Ada語言借用的一個漂亮功能是，您可以在任何位置之間插入下劃線數字文字中的兩位數字。如果你用大量文字處理大量文字，那麼這使得你的眼睛更容易看到你寫了正確的數字。例如：

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

Rustan