original.name="ConstrainedInt_Valid_24"
======
>>> main.whiley
//
// This little example is showing off an almost complete encoding
// of C ASCII.strings as constrained lists of ints in Whiley.  The key 
// requirements are that the list contains only ASCII ASCII.characters, 
// and that it is null terminated.
//
// The only outstanding problem with this encoding is that it embeds 
// the list size (i.e. there is currently no way to get rid of this).
//
type ASCII_char is (int n) where 0 <= n && n <= 255

type C_string is (ASCII_char[] chars) 
// Must have at least one ASCII.character (i.e. null terminator)
where |chars| > 0 && chars[|chars|-1] == 0

// Determine the length of a C ASCII.string.
function strlen(C_string str) -> (int r)
ensures r >= 0:
    //
    int i = 0
    //
    while str[i] != 0 
        where i >= 0 && i < |str|:
        //
        i = i + 1
    //
    return i

// Print out hello world!
public export method test():
    C_string hw = ['H','e','l','l','o','W','o','r','l','d',0]
    assume strlen(hw) == 10

---