The Coq mailing list

[Claude Marche <Claude.Marche AT inria.fr>]

Hi Coq list,

There is no need to use any induction in Coq for proving such a program.
Quick explanation: the computation of weakest precondition does the 
induction for you, using the loop invariant as inductive property.

The solution given by Ruben works, but if you want to prove the original 
code you should reinforce the loop invariant by adding

  a <= x


The, the conjunction of the invariant (a <= x) and the negation of the 
loop condition (not (a < x)) allow one to prove that a == x.

There is a special case to deal with : x == 0, I let that as en exercise.

Last but not least, there is a major misunderstanding of you emphasized 
by the post-condition you put on this method. You seem to believe that 
parameter y is passed by reference. It is not : *in Java, parameters are 
always passed by value*
Please think about that. In essence, you cannot just return void, you 
must return the result.

- Claude

PS: as you can see, the question is not at all related to Coq. You 
should ask on the Why mailing-list instead, that I added as recipient.



On 10/27/2012 12:00 AM, Mariana Bernagozzi wrote:
> Thanks, Ruben!
>
> On Fri, Oct 26, 2012 at 6:13 PM, Ruben Monjaraz
> <ruben.monjaraz AT gmail.com
>  
> <mailto:ruben.monjaraz AT gmail.com>>
>  wrote:
>
>     Try
>
>     while (a != x) {
>
>     instead of
>
>     while (a < x) {
>
>     Ruben
>
>
>
>
>     On Fri, Oct 26, 2012 at 4:47 PM, Mariana Bernagozzi
>     
> <mariana.bernagozzi AT gmail.com
>  
> <mailto:mariana.bernagozzi AT gmail.com>>
>     wrote:
>
>         Hi,
>
>         I'm trying to prove the following program using Krakatoa and Coq:
>
>         /*@ inductive isfact(integer x, integer r) {
>            @  case isfact0: isfact(0,1);
>            @  case isfact1: isfact(1,1);
>            @  case isfactn:
>            @   \forall integer n r;
>            @     n >= 2 && isfact(n-1,r) ==> isfact(n,n*r);
>            @ }
>            @*/
>
>         public class Factorial {
>              /*@ requires x >= 0;
>                @ ensures isfact(x, y);
>                @*/
>              public void fact(int x, int y) {
>                  int a = 1;
>                      y = 1;
>                  //@ loop_invariant 1 <=a && isfact(a,y);
>                  while (a < x) {
>                      a = a + 1;
>                      y = y * a;
>                  }
>              }
>         }
>
>         I've manage to prove all the subgoals but the last one. I think
>         I have to use the *induction* tactic, but I'm not sure how.
>
>         Also, since I'm new using Coq, other comments or suggestions are
>         more than welcome!
>
>         Thanks,
>         Mariana.