3.2. Formal Specification🔗

We formalize validity by a single predicate IsWfDatetime (well-formed grammar syntax) — the range constraint needs no separate clause, since it is implied. The grammar describes a date optionally followed by a time, a fractional-seconds field, and a zone designator, so the specification is phrased over an explicit record of those components (as in the duration grammar).

Every numeric field of this grammar is a digit run of an exact width, so the building block is IsFixedDigits — the Digit{n} refinement of the shared IsDigits predicate (introduced in the Decimal Parsing chapter). It too lives in Cedar.Thm.Data.String:

public def IsFixedDigits (n : Nat) (s : String) : Prop :=
  IsDigits s ∧ s.length = n

Each nonterminal of the grammar becomes a record of its digit fields, with a syntaxWf predicate pinning field widths and a constraintsWf predicate imposing the numeric bounds. For the Date ::= YYYY '-' MM '-' DD production:

public structure DateComponents where
  year : String
  month : String
  day : String

public def DateComponents.syntaxWf (d : DateComponents) : Prop :=
  IsFixedDigits 4 d.year ∧
  IsFixedDigits 2 d.month ∧
  IsFixedDigits 2 d.day

public def DateComponents.constraintsWf (d : DateComponents) : Prop :=
  let mm := fieldValue d.month
  1 ≤ mm ∧ mm ≤ 12 ∧
  1 ≤ fieldValue d.day ∧ fieldValue d.day ≤ daysInMonth (fieldValue d.year) mm

The month/day bounds refer to daysInMonth and isLeapYear, the two auxiliary grammar functions:

public def daysInMonth (y m : Nat) : Nat :=
  if m == 4 || m == 6 || m == 9 || m == 11 then 30
  else if m == 2 then (if isLeapYear y then 29 else 28)
  else 31

public def isLeapYear (y : Nat) : Bool :=
  y % 4 == 0 && (y % 100 != 0 || y % 400 == 0)

The Time, Offset, and Zone nonterminals are modelled the same way; the time-bearing tail (Time ['.' SSS] Zone) is a TimePart combining a TimeComponents, an optional millisecond field, and a Zone:

public structure TimePart where
  time : TimeComponents
  millis : Option String
  zone : Zone

A datetime is then a Date optionally followed by such a tail, and well-formedness reads straight off the grammar — the string is the rendering of some record that is both syntactically well-formed and satisfies the numeric constraints. Phrasing this existentially over asString bakes in the separators, the field order, and the choice among the five top-level forms:

public structure DatetimeComponents where
  date : DateComponents
  time : Option TimePart

public def IsWfDatetime (str : String) : Prop :=
  ∃ components : DatetimeComponents,
    components.syntaxWf ∧
    components.constraintsWf ∧
    str = components.asString

The value of a well-formed string is computed structurally by computeValue: it re-parses the rendering into its components and evaluates the grammar's value formula — days since the epoch (epochDays, the standard civil-calendar day count) scaled to milliseconds, plus the time-of-day, fractional, and zone contributions:

public def computeValue (str : String) : Option Int :=
  (parseComponents str).map DatetimeComponents.toMillis