Function utc_offset_wf 

pub open spec fn utc_offset_wf(bytes: Seq<u8>, pos: usize) -> bool

{
    &&& pos + 5 == bytes.len()
    &&& (bytes[pos as int] == ASCII_PLUS || bytes[pos as int] == ASCII_MINUS)
    &&& digits(bytes, pos as int + 1, pos as int + 5)
    &&& decimal2(bytes, (pos as int + 1) as usize) <= 23
    &&& decimal2(bytes, (pos as int + 3) as usize) <= 59

}

Spec function validating a UTCTime timezone offset (+hhmm or -hhmm).