/*@
   requires \exists integer i; Length_of_str_is(s,i);
   assigns \nothing;
   ensures \exists integer i; Length_of_str_is(s,i) && \result == i;
 @*/
int strlen(const char *s) {
  const char *ss = s;
  /*@
      loop invariant s <= ss <= s+Length(s);
      loop invariant \forall integer i; 0 <= i < (ss-s) ==> s[i] != 0;
      loop assigns ss;
      loop variant Length(s) - (ss-s);
   @*/
  while (*ss)
    ss++;
  return ss - s;
}