original.name="Complex_Valid_8"
======
>>> main.whiley
type char is int
type string is int[]

// Represents a transition from one
// state to another for a given character.
type Transition is ({
    int from,
    int to,
    char character
} t) where
    t.from >= 0 && t.to >= 0 &&
    t.from < t.to

// A Finite State Machine representation of a Trie
type Trie is {
    Transition[] transitions
} where validTransitions(transitions)

property validTransitions(Transition[] transitions) -> (bool r):
    return all { k in 0..|transitions| | transitions[k].to <= |transitions| }

// Define the Empty Trie
final Transition DummyTransition = { from: 0, to: 1, character: 0 }
final Trie EmptyTrie = { transitions: [DummyTransition; 0] }

function append(Transition[] transitions, Transition t) -> (Transition[] result)
requires t.to <= (|transitions| + 1)
requires validTransitions(transitions)
ensures validTransitions(result)
ensures |result| == |transitions| + 1:
    Transition[] r = [t; |transitions| + 1]
    int i = 0
    while i < |transitions|
    where i >= 0 && |r| == (|transitions|+1)
    where validTransitions(r):
        r[i] = transitions[i]
        i = i + 1
    //
    return r

// Add a complete string into a Trie starting from the root node.
function add(Trie trie, string str) -> Trie:
    return add(trie,0,str,0)

// Add a string into a Trie from a given state, producing an
// updated Trie.
function add(Trie trie, int state, string str, int index) -> Trie
requires state >= 0 && state <= |trie.transitions|
requires index >= 0 && index <= |str|:
    //
    if |str| == index:
        return trie
    else:
        //
        // Check whether transition exists for first
        // character of str already.
        char c = str[index]
        int i = 0
        //
        while i < |trie.transitions| where i >= 0:
            Transition t = trie.transitions[i]
            if t.from == state && t.character == c:
                // Yes, existing transition for character
                return add(trie,t.to,str,index+1)
            i = i + 1
        //
        // No existing transition, so make a new one.
        int target = |trie.transitions| + 1
        Transition t = { from: state, to: target, character: c }
        trie.transitions = append(trie.transitions,t)
        return add(trie,target,str,index+1)

// Check whether a given string is contained in the trie,
// starting from the root state.
function contains(Trie trie, string str) -> bool:
    return contains(trie,0,str,0)

// Check whether a given string is contained in the trie,
// starting from a given state.
function contains(Trie trie, int state, string str, int index) -> bool
requires index >= 0 && index <= |str|
requires state >= 0:
    //
    if |str| == index:
        return true
    else:
        // Check whether transition exists for first
        // character of str.
        char c = str[index]
        int i = 0
        //
        while i < |trie.transitions| where i >= 0:
            Transition t = trie.transitions[i]
            if t.from == state && t.character == c:
                // Yes, existing transition for character
                return contains(trie,t.to,str,index+1)
            i = i + 1
        //
        return false

public export method test():
    Trie t = EmptyTrie
    // First, initialise trie
    t = add(t,"hello")
    t = add(t,"world")
    t = add(t,"help")
    // Second, check containment
    assume contains(t,"hello")
    assume !contains(t,"blah")
    assume contains(t,"hel")
    assume !contains(t,"dave")

---