mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
24 lines
343 B
C
24 lines
343 B
C
|
|
// la multiplication dite russe
|
|
|
|
int mult(int a, int b)
|
|
//@ ensures result == a * b;
|
|
{ int p = a;
|
|
int q = b;
|
|
if (q < 0) {
|
|
p = -a;
|
|
q = -b;
|
|
}
|
|
int r = 0;
|
|
while (q) {
|
|
//@ invariant 0 <= q;
|
|
//@ invariant r + p * q == a * b;
|
|
//@ variant q;
|
|
if (q % 2 == 1)
|
|
r += p;
|
|
p *= 2;
|
|
q /= 2;
|
|
}
|
|
return r;
|
|
}
|