Java: Miscellaneous: Text
Text

class Annotation -- not serializable?
{
    ::new(with: Object/null) ensures value == with

    value: Object/null
    redefined toString: String
        ensures value != null => result.equals(value.toString)}
}

class Attribute -- why an inner class of AttributedCharacterIterator?
{
}

class CharacterIterator -- asymmetric (can be after the last, but not before the first)
{
     redefined clone: CharacterIterator
         ensures result.beginIndex == beginIndex, result.endIndex == nedIndex, result.index == index
             -- and same contents

     beginIndex: int
     endIndex: int

     current: char
     index: int

     setIndex(value: int) requires beginIndex <= value <= endIndex ensures index == value
     
     first    ensures index == beginIndex
     last     ensures index == max(beginIndex, endIndex - 1) -- max only matters for empty
     next     ensures index == min(endIndex, oldIndex + 1)
     previous ensures index == max(beginIndex, oldIndex - 1)

     invariant
         beginIndex <= index <= endIndex
         current == DONE <=> index == endIndex
}

class AttributedCharacterIterator
    extends CharacterIterator
{
    allAttributeKeys: Set
  
    attributes: Map
    attribute(Attribute a): Object/null ensures result == attributes.get(a)

    
    runStart -- not runBegin?
    runLimit: int -- would have benefitted from a Range class, not runEnd?
    runStart(Attribute a): int
    runLimit(Attribute a): int

    runStart(Set attributes): int
        ensures result = max_{a in attributes}(runStart(a))

    runLimit(Set attributes): int
        ensures result = min_{a in attributes}(runStart(a))

    invariant
         runStart <= index < runLimit
         forall Attribute a: beginIndex <= runStart(a) <= runStart <= runLimit <= runLimit(a) <= endIndex
}

class AttributedString
{
    ::new(AttributedCharacterIterator a, int from, int to, Set with)
    -- not even within a class the order of arguments is consistent      
    
    ::new(String s, Map a) ensures s == text -- attributes in 'a' are taken

    sneaky text: String
    
    addAttribute(Attribute a, Object/null value, [int from, int to])
    addAttributes(Map m, int from, int to)
    
    iterator([Set with, [int from, int to]]): AttributedCharacterIterator
       ensures result.endIndex - result.beginIndex == to - from 
}


class StringCharacterIterator
    extends CharacterIterator
{
    ::new(String value) ensures text == value
    setText(String value) ensures text == value 
    text: String

    invariant text.length == endIndex - beginIndex -- much more
}