search

AllanBlanchard / tutoriel_wp

Frama-C and WP tutorial
Other
55 stars 16 forks source link

Exercise 3.4.1.4: Add missing postcondition to ex-4-change-answer.c #32

Closed wizeman closed 3 years ago

wizeman commented 3 years ago

Otherwise, this trivial implementation would be valid:

int make_change(int amount, int received, int change[9]){
  if(amount > received) return -1;

  int rest = received - amount ;

  change[N500] = 0;
  change[N200] = 0;
  change[N100] = 0;
  change[N50] = 0;
  change[N20] = 0;
  change[N10] = 0;
  change[N5] = 0;
  change[N2] = 0;
  change[N1] = rest;

  return 0;
}
wizeman commented 3 years ago

Edit: just fixed a bug in the postcondition (I had forgotten the values[i] multiplications).

AllanBlanchard commented 3 years ago

Oh yes indeed !

For this one, I think that there are no other code with similar idea, so I can merge it immediately.

Thank you!