abst@ype strlen(n: int)
viewdef string_v(n:int, l:addr) = strlen(n) @ l
vtypedef string_vt(n: int, l:addr) = (string_v(n, l) | ptr(l))

vtypedef String_vt = [n:nat][l:addr | l > null] string_vt(n, l)