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 previ
Hello David,
In short, if you write
assert { A by B so C }
then after using "split" you will have to prove :
. B
. B -> C
. B /\ C -> A
but more importantly, in the code after the assert, the only visible
extra hypothesis will be A. B and C will not be visible.
This addition of "by" an
Hello Claude,
Le 16/11/2016 à 10:08, Claude Marché a écrit :
> assert { A by B so C }
>
> then after using "split" you will have to prove :
>
> . B
> . B -> C
> . B /\ C -> A
>
> but more importantly, in the code after the assert, the only visible
> extra hypothesis will be A. B and C wil
Le 16/11/2016 à 10:08, Claude Marché a écrit :
> This addition is due to Martin Clochard, a paper explaining that should
> appear very soon (in French first, sorry for non-french speaking
> user...)
For info, the paper in question is there :
https://hal.inria.fr/hal-01404935
--
Claude Marché
