The ACSL specification would be something like:

/*@
requires valid_string(s);
behavior good_number:
  assumes \exists integer n; string_is_number(s, n) && LONG_MIN <= n <= LONG_MAX;
  assigns \result;
  ensures \exists integer n; string_is_number{Pre}(s, n) && \result == n;
behavior bad_number:
  assumes \forall integer n; ! string_is_number(s, n);
  assigns error;
  ensures error==1;
*/
long str2long (const char * s);

The predicate valid_string is conveniently predefined :

/*@ predicate valid_string{L}(char *s) =
      0 <= strlen(s) && \valid(s+(0..strlen(s)));
*/

(The predicate strlen is itself defined in a way such that it makes sense to use it as it is used here)

The predicate string_is_number would have to be defined by the specifier. Yes, it would be the same length as (and would like a) prolog implementation of that idea. On the plus side, the predicate could be re-used as-is for the specification of str2int and str2longlong.

In effect, when verifying an implementation of str2long against such a specification, you would in some sense be comparing an implementation with another. If there is the same bug in both, it might go unnoticed. But I have to point out that, in most programming languages, and especially in C, nothing prevents you to put together a function f() and a function g() that, while each fine in itself, do not work well together:

void f(int*p) // accepts NULL or a valid pointer to int
{
  g(p);
}

void g(int *p) // expects a valid pointer
{
  *p = 1;
}

By contrast, with ACSL specifications, the user would be warned when trying to put f() and g() together. Similarly, you my get predicate string_is_number wrong and thus manage to prove that a function that should be rejected, but hopefully you will catch that when str2long is used and the wrong definition for string_is_number prevents another property from being proved.