The Coq mailing list

[Ruben Monjaraz <ruben.monjaraz AT gmail.com>]

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> 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.