• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
        • Deftreeops
        • Defdefparse
        • Defgrammar
        • Tree-utilities
        • Notation
        • Grammar-parser
        • Meta-circular-validation
        • Parsing-primitives-defresult
        • Parsing-primitives-seq
        • Operations
          • In-terminal-set
          • Well-formedness
            • Rulelist-incremental-ok-p
            • Num-val-wfp
            • Char-val-wfp
            • Prose-val-wfp
            • Rulename-wfp
            • Rulelist-wfp
            • Repeat-range-wfp
            • Rule-list-wfp
            • Concatenation-wfp
            • Alternation-wfp
            • Rule-wfp
            • Concatenation-list-wfp
            • Repetition-list-wfp
            • Repetition-wfp
            • Element-wfp
          • Closure
          • Plugging
          • Ambiguity
          • Renaming
          • Numeric-range-retrieval
          • Rule-utilities
          • Removal
          • Character-value-retrieval
        • Examples
        • Differences-with-paper
        • Constructor-utilities
        • Grammar-printer
        • Parsing-tools
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Operations

Well-formedness

Well-formed ABNF grammars.

Certain ABNF grammars are valid according to the formalized abstract syntax, but (include parts that) violate certain conditions that are either required by the concrete syntax defined in [RFC:4] or otherwise reasonably justifiable. These additional conditions are captured by the notion of well-formedness.

Subtopics

Rulelist-incremental-ok-p
Check if incremental rules appear after non-incremental rules with the same names.
Num-val-wfp
A direct numeric value notation is well-formed iff it consists of at least one number; a range numeric value notation is well-formed iff the minimum does not exceed the maximum.
Char-val-wfp
A character value notation is well-formed iff it consists of only non-control ASCII characters, except for the double quote character.
Prose-val-wfp
A prose value notation is well-formed iff it consists of only non-control ASCII characters, except for the right angle bracket character.
Rulename-wfp
A rule name must start with a lowercase letter (and thus not be empty) and contain only lowercase letters, numbers, and dashes.
Rulelist-wfp
A rule list is well-formed iff all its rules are well-formed, there are no duplicate rules, and incremental rules follow non-incremental rules.
Repeat-range-wfp
A repetition range is well-formed iff the minimum does not exceed the maximum.
Rule-list-wfp
Check if all the rules in a list of rules are well-formed.
Concatenation-wfp
A concatenation is well-formed iff it is not empty and all its repetitions are well-formed.
Alternation-wfp
An alternation is well-formed iff it is not empty and all its concatenations are well-formed.
Rule-wfp
A rule is well-formed iff its name and definiens are well-formed.
Concatenation-list-wfp
Check if all the concatenations in a list of concatenations are well-formed.
Repetition-list-wfp
Check if all the repetitions in a list of repetitions are well-formed.
Repetition-wfp
A repetition is well-formed iff its repetition range and its element are well-formed.
Element-wfp
An element is well-formed iff its constituents are well-formed.