Implementing strlen safely

Google Group
1

When encountering a programming language, I often ask the question:
How strlen, which computes the length of a given C-style string, should be
implemented
in this language?

Here is a way to implement strlen safely in ATS:

fun
strlen{n:nat}
(
str: string(n)
) : int(n) = let
//
fun loop{i,j:nat}
(str: string(i), j: int(j)): int(i+j) =
if isneqz (str) then loop (str.tail, succ(j)) else j
//
in
loop (str, 0)
end // end of [strlen]

If a language does not allow you to implement strlen, then the language is
probably not well-suited
for low-level programming.

However, most languages suited for low-level programming usually do not
allow you to implement strlen
safely.

2

Hi Artyom,

str.tail expands to string_tail(str):

fun string_tail {n:pos} (string(n)): string(n-1)
overload .tail with string_tail

This is called dot notation overloading in ATS.On Tuesday, February 18, 2014 1:27:18 AM UTC-5, Artyom Shalkhakov wrote:

Hello Hongwei,

понедельник, 17 февраля 2014 г., 4:33:11 UTC+6 пользователь gmhwxi написал:

When encountering a programming language, I often ask the question:
How strlen, which computes the length of a given C-style string, should
be implemented
in this language?

Here is a way to implement strlen safely in ATS:

fun
strlen{n:nat}
(
str: string(n)
) : int(n) = let
//
fun loop{i,j:nat}
(str: string(i), j: int(j)): int(i+j) =
if isneqz (str) then loop (str.tail, succ(j)) else j
//
in
loop (str, 0)
end // end of [strlen]

I’m wondering what does this [str.tail] syntax stand for? In ATS1 there
was a function that basically returned an incremented pointer to the string
(i.e., a tail of the string). Does the syntax expand to a regular function
call?

If a language does not allow you to implement strlen, then the language
is probably not well-suited
for low-level programming.

However, most languages suited for low-level programming usually do not
allow you to implement strlen
safely.

3

Hello Hongwei,

When encountering a programming language, I often ask the question:
How strlen, which computes the length of a given C-style string, should be
implemented
in this language?

Here is a way to implement strlen safely in ATS:

fun
strlen{n:nat}
(
str: string(n)
) : int(n) = let
//
fun loop{i,j:nat}
(str: string(i), j: int(j)): int(i+j) =
if isneqz (str) then loop (str.tail, succ(j)) else j
//
in
loop (str, 0)
end // end of [strlen]

I’m wondering what does this [str.tail] syntax stand for? In ATS1 there was
a function that basically returned an incremented pointer to the string
(i.e., a tail of the string). Does the syntax expand to a regular function
call?