Hello,
I noticed that the isqrt example has been recently rewritten with a new
syntax "assert { ... by ... so ... }":
https://scm.gforge.inria.fr/anonscm/gitweb?p=why3/why3.git;a=commitdiff;h=bbb659aa149113551262f00f906952db55f89c90#patch1
What is the purpose of this new syntax compared to previous use of
assertions and ghost variables? Does this bring any advantage with
respect to provers?
Best regards,
david
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/mailman/listinfo/why3-club
