Values and time

7. Time, made symbolic

Real machines need delays: “shut down only if the fault persists for 2 seconds.” zqel has two declarative time primitives:

• HELD(cond, PT) — a BOOL that is true once cond has been continuously true for at least the duration PT.
• ELAPSED(cond, PT) — the matching TIME value: how long cond has been continuously true, capped at PT (this is the IEC TON.ET output).

Together they are an on-delay timer. Here is a full IEC TON (examples/iec/ton.zqel):

FUNCTION_BLOCK TON
VAR_INPUT
    IN : BOOL;                     // start condition
    PT : TIME;                     // preset time (a runtime value, not a constant!)
END_VAR
VAR_OUTPUT
    Q  : BOOL;                     // true PT after IN went true and stayed true
    ET : TIME;                     // elapsed time so far, capped at PT
END_VAR
IMPLEMENTATION
    Q  := HELD(IN, PT);            // "IN has held for >= PT"
    ET := ELAPSED(IN, PT);         // "how long IN has held, up to PT"
END_IMPLEMENTATION
END_FUNCTION_BLOCK

The generated ST does not re-implement timing arithmetic — it maps straight onto a native IEC TON instance, the same standard block you already use:

VAR
    _held_in_0 : TON;              (* a real IEC TON, instantiated for us *)
END_VAR
    _held_in_0(IN := IN, PT := PT);
    Q := _held_in_0.Q;
    ET := _held_in_0.ET;

So on the PLC there is no elapsed-time arithmetic leaking into your logic; time stays inside a proper timer block.

Why this lets us prove timing-independent properties

Here is the beautiful part. Inside the verifier, time is symbolic — the proof does not pick a specific delay, it reasons about all delays at once. Consider a pressure guard that warns immediately but shuts down only after a sustained fault (examples/pressure.zqel):

    Warn:
        ON WHEN Overpressure PRIO 1;       // warn the instant pressure is high
        OFF OTHERWISE;

    Shutdown:
        ON WHEN HELD(Overpressure, 2s) PRIO 1;   // shut down only after 2 s of it
        OFF OTHERWISE;

    RULE Shutdown ONLY_WHEN Warn;      // necessary: shutting down requires warning
    RULE Overpressure IMPLIES Warn;    // sufficient: overpressure alone raises it

These are the two sides a safety sentence can have, and zqel spells them apart:

• X ONLY_WHEN C — a necessary condition. X may only hold while C does. Read it as the sentence “shutting down is allowed only while warning”.
• C IMPLIES X — a sufficient one. C alone is enough to force X. Read it as “overpressure is by itself enough to raise the warning”.

The literal being constrained stands on the left of ONLY_WHEN and on the right of IMPLIES; the condition stands on the other side. Both clauses are proven against the definitions above — they are claims about the block, not extra assumptions layered on top of it. Write a false one and the compiler refuses it: RULE Warn IMPLIES Shutdown is rejected with [invariant-step], because the warning rises two seconds before the shutdown does.

You can still write the same claim as a raw boolean — INVARIANT NOT Shutdown OR Warn; is accepted and means exactly the clause above. The clause form says which kind of condition you meant, and that is what the next reader needs.

✅ Proven for every possible timing: whenever the block shuts down, it is also warning. It does not matter whether the 2-second timer has elapsed or not, whether the scan is fast or slow — a shutdown can only happen while overpressure is present, and overpressure always raises the warning in the same scan.

The generated ST again uses a native TON and shows the 2s preset as the IEC literal T#2000ms:

    (* proven rule: (NOT Shutdown OR Warn) *)
    (* proven rule: (NOT Overpressure OR Warn) *)
    _held_overpressure_0(IN := Overpressure, PT := T#2000ms);
    _Warn_next := Overpressure;
    _Shutdown_next := _held_overpressure_0.Q;
    Warn := _Warn_next;
    Shutdown := _Shutdown_next;

---

8. Continuous values: MATHREAL, DT, CLAMP

For control (levels, flows, temperatures) you need continuous quantities. MATHREAL is zqel's continuous number. Two primitives make control code expressible:

• DT — the elapsed time of the current scan, in seconds, taken from the runtime clock. You never wire it; it is always available. In proofs it is symbolic and non-negative, so results hold for any scan rate.
• CLAMP(x, lo, hi) — saturation: return x, but never below lo or above hi.

A clamped integrator accumulates its input over time and is limited to a band (examples/analog/integrator.zqel):

FUNCTION_BLOCK Integrator
VAR_INPUT
    x     : MATHREAL;                  // the signal to integrate (e.g. a rate)
    Limit : MATHREAL;                  // the saturation band, supplied by the caller
END_VAR
VAR_OUTPUT
    y : MATHREAL;                      // the accumulated integral
END_VAR
IMPLEMENTATION
    y:
        // new y = old y + x*dt, but never outside [-Limit, +Limit]
        SET CLAMP(y + x * DT, -Limit, Limit) OTHERWISE;

    ASSUME
        Limit >= 0.0;              // a precondition the caller must satisfy (see below)

    INVARIANT
        y <= Limit;                // the integral never winds up past the band ...
    INVARIANT
        y >= -Limit;               // ... in either direction
END_IMPLEMENTATION
END_FUNCTION_BLOCK

y + x * DT is the discrete integration step: add “rate × elapsed time” to the running total. Wrapping it in CLAMP(..., -Limit, Limit) implements anti-windup — a standard control technique that stops an integrator from accumulating without bound when it saturates.

✅ Proven: −Limit <= y <= Limit for any input signal and any scan timing. The anti-windup is not hoped-for behaviour; it is a theorem about the block.

A MATHREAL in zqel is mathematical ℝ — not a machine float and not a fixed-point integer. Proofs hold over the real numbers exactly. This is also why DT is symbolic in the proof: the solver reasons over all possible ℝ-valued scan times at once, so the anti-windup bound holds regardless of how fast or slow the scan runs.

To emit runnable code for a block with MATHREAL variables you must first declare a Representation Boundary — the choice of machine arithmetic. The simplest way is the --profile float64 flag, which lowers MATHREAL to LREAL — IEEE 754 binary64, rendered as LREAL in ST and f64 in Rust. Without a Representation Boundary the compiler verifies the programme mathematically but refuses to generate code, because the gap between ℝ and a finite machine type is a separate correctness obligation (see how-to/real-numerical-assurance.md). ST and Rust are then generated from the same proven ℝ model, so they cannot diverge from each other or from the proof. For the complete MATHREAL/LREAL semantics and the numerical assurance chain, see Language Reference §13.

---

9. Partial operations: division and IF/THEN/ELSE

Division has a trap: a / b is undefined when b = 0. In most languages that is a runtime crash waiting to happen. zqel treats “the divisor is non-zero” as a proof obligation, just like an invariant. Writing a bare division that might divide by zero is a compile error:

[division-by-zero] cannot prove the divisor is non-zero: b may be 0 where
a / b is evaluated. Guard it, e.g. IF b <> 0.0 THEN ... ELSE ...

The language gives you the tool to discharge the obligation: IF cond THEN a ELSE b is a conditional expression (it produces a value), and the proof is path-sensitive — inside the THEN branch the compiler knows cond is true. So a discrete-time differentiator guards its division and compiles (examples/analog/differentiator.zqel):

    // rate of change = (x - x_prev) / dt, but only when dt is non-zero
    d: SET IF DT <> 0.0 THEN (x - x_prev) / DT ELSE 0.0 OTHERWISE;

Because you handled the DT = 0 case explicitly (returning 0.0), the compiler is satisfied that the division is only ever reached when DT <> 0. And the generated code contains exactly that guard — nothing is swept under the rug, and there is no possibility of a divide-by-zero fault on the machine.

The pattern: zqel never silently accepts an operation that can fail. It makes you prove it is safe, and gives you the language (IF, guards, priorities) to do so.

---

10. Environment premises: ASSUME

Look back at the integrator's line ASSUME Limit >= 0.0;. What is it?

An INVARIANT is something the block must prove. An ASSUME is the opposite: something the block's caller must guarantee. This is called an assume-guarantee contract, and it is what lets a block be reusable with parameters instead of magic numbers.

For students, the shortest way to keep the two apart is:

• INVARIANT = my block guarantees this
• ASSUME = my block only promises that if the caller gives me this

Why does the integrator need it? Its anti-windup proof only works if the band is sensible. If Limit could be negative, then at power-on y = 0 would already be outside [-Limit, Limit] (an empty interval), and CLAMP's bounds would be crossed. Rather than hard-code Limit = 10, the block states its honest precondition — “I work for any non-negative Limit” — and the compiler then proves the anti-windup for every valid Limit at once.

Rules that keep ASSUME sound:

• It may mention inputs only. Assuming something about the block's internal state would be cheating (the environment does not control internal state).
• It may not mention DT either — the compiler rejects it. You must not “assume away” properties of the runtime clock.
• The assumptions must be satisfiable together. Contradictory assumptions (from which anything follows) are a contradictory-assume error, so you cannot accidentally prove everything by assuming a falsehood.

So if you are unsure which one to write, ask:

“Can the block itself enforce this?”

If yes, it belongs in the rules and may then be stated again as an INVARIANT. If no — if it is really a requirement on the outside world — it is an ASSUME.

---