The Coq mailing list

[Mariana Bernagozzi <mariana.bernagozzi AT gmail.com>]

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.

Attachment: Factorial_WP_Jessie_program_WP_parameter__Factorial_fact_ensures_default_7.v
Description: Binary data