Citation :Qu'est ce qui te prouve, en cas de modification, que la régression ne va pas porter sur cette preuve?
Citation :Si je fais une modification sur vehicle.destroy(), je dois effectivement refaire la preuve
si tu la change tu la refais. Mais comme l'a dit Sephi c'est un outil.
tiens si tu veux du code, nous en étions à tester l'opérateur * tu peux essayer de prouver que mon implémentation est correcte pour les cas de base et que pour tous X et Y , mult Y X == Y + mult Y (X-1) etc.. (pas dur vu que mon implémentation se contente justement de reprendre cette preuve
Code :
-module(mymath).
-export([test/0,mult/2]).
mult(0, _) -> 0;
mult(_, 0) -> 0;
mult(X, Y) when Y > 0 -> X + mult(X, Y-1);
mult(X, Y) when Y < 0 -> 0 - mult(X, 0-Y).