[Easycrypt-club] How to use local variable in a lemma

sarah chabane sarah.chabane22 at gmail.com
Mon Jan 22 10:59:55 CET 2018


Hi,

I need to use a local variable of a procedure in a lemma,


for example , for this module :

module G = {
 proc g() : int ={
  var r, x : int;
  if (x < 0) {
   r = 5; } else {
   r = 10;
  }
  return r;
 }
}.

I want to proof this lemma:

lemma ex : forall v,
 hoare [ G.g : v = x ==> if v < 0  then  res = 5 else res <> 5 ].


How can i use the x of the proc G.g ?


Best regards.
Sarah.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/easycrypt-club/attachments/20180122/3f745d7f/attachment.html>


More information about the Easycrypt-club mailing list