The Complete Level: The Full Language¶

The complete level is Frml's default level. It selects the full language: scalars, loops, fixed-size arrays, and the built-in functions. The individual features are explained in the earlier tutorials:

• scalar: scalars, branching, assert, division.
• contracts: contracts, function calls, recursion, quantifiers.
• loop: while loops and invariants.
• array: fixed-size arrays.
• builtin: I/O built-ins and push/pop.

complete currently has the same features as the builtin level. It is kept as the top of the level hierarchy so that new features can be added here without disturbing the staged type checkers and provers below it.

Two files implement the level:

• frml/typechecker_complete.py is a trivial subclass of the builtin type checker.
• frml/prover_complete.py is a trivial subclass of the builtin prover. The shared Z3 check loop lives in frml/z3check.py.

Because complete is the default, no --level flag is needed:

frml check examples/complete/required.frml

This is equivalent to:

frml check --level builtin examples/complete/required.frml