• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
          • Parser-output-to-values
          • Values
          • Syntax
          • Patbind-pattern
          • Operations
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Kestrel-books
  • Projects

Json

A library for JSON.

The JavaScript Object Notation (JSON) is described by:

  • The JSON web site.
  • The ECMA-404 Standard (2nd Edition, December 2017).
  • The ISO/IEC 21778:2017 Standard.
  • The RFC 8259, including errata.

These are all meant to be consistent, at least in defining the JSON format, although they may contain slightly different notations and recommendations.

Currently this library contains:

  • A formalization of the syntax of JSON, based on the ABNF grammar in the RFC.
  • A formalization of JSON values.
  • Some operations on JSON values, including some lightweight checkers.
  • A translator from the output of the JSON parser in kestrel/json-parser/ to the JSON value representation defined in this library.
  • b* binders for the representation of JSON values defined in this library.

Subtopics

Parser-output-to-values
A translator from the JSON parser's output to our model of JSON values.
Values
JSON values.
Syntax
Syntax of JSON.
Patbind-pattern
b* binder for JSON pattern matching.
Operations
Operations on JSON values.