[Easycrypt-club] Questions sur la langue EasyCrypt

Catherine Meadows catherine.meadows at nrl.navy.mil
Ven 27 Avr 00:12:37 CEST 2012


J'essaie d'apprendre à utiliser EasyCrypt. La majeure partie est soit auto-explicatif ou peut être trouvée dans la littérature. La principale exception est la tactique. Quelqu'un peut-il me donner une description de ce qui sont les tactiques les plus couramment utilisés et ce qu'ils font?

Les tactiques suivantes viennent de la BNF dans la documentation de travail.

Concernant les tactiques, je crois que je comprends:

1. "inline" Cette fonction est remplace par sa définition.
2. "trivial" Vérifiez que les deux jeux sont trivialement identiques
3.  L'argument optionnel {<number> '}' fait référence au jeu auquel la tactique est appliquée.
Si l'argument n'est pas là, la tactique est appliquée aux deux jeux.

Ce sont les tactiques que je comprends partiellment:

1."swap": je suppose que cela signifie que deux lignes sont echanges dans un jeu, mais la notation
ne supporte pas cela. Les arguments sont soit un intervalle suivie par un nombre entier, ou un nombre entier seul.
2.«Simpl»: je suppose que cela signifie «simplifier». Mais par quelle methode est EasyCrypt capable de simplifier un jeu? Est-ce tout simplement la suppression du code mort?
3."try" Je suppose que cela signifie essayer d'appliquer une tactique, et si il n'est pas possible de l'appliquer,  il passe à la prochaine commande. Est-ce juste?
4."let" Ceci est utilisé pour affecter un identifiant à une expression. Est-ce vrai?
5. "!" Est-ce la négation?

Tactiques que je ne comprends pas:
"idtac"
"call"
"asgn"
"rnd"
"auto"
"rauto"
"derandomize"
"wp"
"case"
"apply"
"prHL"
"apRHL"
"unroll"
"strengthen"
"app"
"*"
"admit"
"expand"

Il semble également que vous pouvez utiliser quelques-uns des termes définis dans la BNF pour écrire des tactiques plus complexes.

Par exemple:
"If", "case", "while"  
Est-cs vrai?

En outre, quelle est la signification des virgules et des  deux-pointsdans la définition de "app"?

Merci en avance pour toute aide que vous pouvez me donner,

Cathy Meadows


Catherine Meadows
Naval Research Laboratory
Code 5543
4555 Overlook Ave., S.W.
Washington DC, 20375
phone: 202-767-3490
fax: 202-404-7942
email: catherine.meadows at nrl.navy.mil

-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/easycrypt-club/attachments/20120426/5efd3095/attachment.html>


More information about the Easycrypt-club mailing list