Contrôle de la convention de dénomination Dafny et utilisation de constantes

Question

Existe-t-il un moyen de contrôler la convention de dénomination utilisée par Dafny pour le code cible?

Est-il possible d'utiliser globalement une constante symbolique? Quelque chose comme ceci:

? global const MaxValue = 10000; ? 

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

Y at-il un moyen de convertir une expression numérique en chaîne?

Answer 1

Oui et oui.

Pour contrôler les noms des différentes entités que Dafny utilise dans le code cible, utilisez l'attribut {:extern "ThisIsTheNameIWant"}. Cet attribut est pris en charge sur la plupart des déclarations. Par exemple, vous pouvez en mettre un sur une classe et un autre sur une méthode à l'intérieur de la classe. Pour plus d'exemples, voir le fichier Test/dafny0/Extern.dfy dans la suite de tests Dafny. Si vous voulez voir ce qui est généré, utilisez le drapeau /spillTargetCode:1 depuis la ligne de commande.

Pour les constantes, utilisez:

const MaxValue := 10000 

(Remarque, jusqu'à récemment, il fallait fournir le type de constantes explicitement, de sorte que vous deviez écrire

const MaxValue: int := 10000 

Si vous construisez la la dernière version de Dafny à partir des sources, le type est déduit de l'expression de droite.)

Une fonctionnalité intéressante, empruntée au langage Ada, est que vous pouvez insérer un trait de soulignement entre deux chiffres en littéraux numériques. Si vous travaillez avec de gros littéraux avec un tas de zéros, cela permet à vos yeux de voir plus facilement que vous avez écrit le bon nombre. Par exemple:

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

Rustan