25 lines
468 B
C
25 lines
468 B
C
#ifndef __FORMALISM__
|
|
#define __FORMALISM__
|
|
|
|
#include <limits.h>
|
|
|
|
/*@ logic integer abs(integer n) = 0<n?n:-n;*/
|
|
|
|
/*@
|
|
requires INT_MIN < n < INT_MAX;
|
|
terminates \true;
|
|
ensures \result == abs(n);
|
|
assigns \nothing;
|
|
*/
|
|
int abs(int n);
|
|
|
|
/*@
|
|
requires INT_MIN < n < INT_MAX;
|
|
requires INT_MIN <= n * (int)((int)n % 2 + ((int)n + 1)%2) <= INT_MAX;
|
|
terminates \true;
|
|
ensures \result == abs(n);
|
|
assigns \nothing;
|
|
*/
|
|
int abs2(int n);
|
|
|
|
#endif
|