From this page, you can run Whiley programs in your browser! For more on Whiley, visit whiley.org.

// Define the null terminator constant NULL is 0 // Define the ASCII 8bit character type ASCII_char is (int n) where 0 <= n && n <= 255 // Define the C null-terminated string type C_string is (ASCII_char[] str) // Must have at least one character (i.e. null terminator) where |str| > 0 && some { i in 0 .. |str| | str[i] == NULL } // Determine the length of a C string. function strlen(C_string str) -> (int r) // Null terminator is at end of string ensures str[r] == NULL // No null terminator within the length returned ensures all { k in 0 .. r | str[k] != NULL }: // int i = 0 // while str[i] != NULL where i >= 0 && i < |str| where all { k in 0 .. i | str[k] != NULL}: i = i + 1 // return i
Enable Verification