Dafny-Namenskonvention steuern und Konstanten verwenden

Question

Gibt es eine Möglichkeit, die Namenskonvention zu steuern, die Dafny für den Zielcode verwendet?

Ist es möglich, eine symbolische Konstante global zu verwenden? So etwas wie dieses:

? global const MaxValue = 10000; ? 

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

Gibt es eine Möglichkeit, einen numerischen Ausdruck in eine Zeichenfolge zu konvertieren?

Answer 1

Ja und ja.

Um die Namen verschiedener Entitäten zu steuern, die Dafny im Zielcode verwendet, verwenden Sie das Attribut {:extern "ThisIsTheNameIWant"}. Dieses Attribut wird von den meisten Deklarationen unterstützt. Zum Beispiel können Sie einen auf eine Klasse und einen anderen auf eine Methode innerhalb der Klasse setzen. Weitere Beispiele finden Sie in der Datei Test/dafny0/Extern.dfy in der Dafny-Testsuite. Wenn Sie sehen möchten, was generiert wird, verwenden Sie das Flag /spillTargetCode:1 von der Befehlszeile.

Für Konstanten verwenden:

const MaxValue := 10000 

(Beachten Sie, bis vor kurzem Sie die Art der Konstanten explizit liefern hatte, so dass Sie

const MaxValue: int := 10000 

schreiben hatte Wenn Sie das Gebäude sind neueste Version von Dafny aus Quellen, der Typ wird aus dem Ausdruck auf der rechten Seite abgeleitet.)

Eine nette Eigenschaft, die aus Ada-Sprache entlehnt ist, dass Sie einen Unterstrich zwischen beliebigen einfügen können zwei Ziffern in numerischen Literalen. Wenn Sie mit großen Literalen arbeiten, in denen eine Nulle enthalten ist, wird es für Ihre Augen einfacher zu sehen, dass Sie die richtige Zahl geschrieben haben. Zum Beispiel:

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

Rustan