--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on July 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Integerdivision



On Christoph Weber's request I forward the following mail:
-----------------------------

Integerdivision

Hello, I am exploring the limitations of divisions and annotations and I
would
like to know, how many VC can be proven with your development tools:
But I pay special attention to the terms connected with the division.

Sincerely

Christoph

//====================================================================
/*@
	lemma division:   \forall integer x; 0 < x ==> 0 <= x/2;
*/

/*@
	requires limit > 0;
	ensures limit == \result;
*/

int integerdivision(int limit)
{
	int b = 1;
	int a = limit;
	int index = 0;
	int old_a=a;
	int old_b=b;
	/*@
		loop invariant a/2 >= 0;
		loop invariant 0 <= a <= limit;
		loop invariant 1 <= b <= limit;
		loop invariant index == 0 ==> b == old_b;
		loop invariant index == 0 ==> a == old_a;
		loop invariant index > 0 ==> b == old_b/2;
		loop invariant index > 0 ==> a == old_a*2;
	*/
	while (0 < a)
	{
		old_a=a;
		old_b=b;
		a = a/2;
		b = b*2;
		index ++;
	}
	return b;
}
//====================================================================