|
|
|---|
|
|
|
|---|
Concrete syntax of JSON.
We use our verified grammar parser to turn the ABNF grammar of JSON (from the JSON RFC) into a formal representation in ACL2.
As the grammar is technically ambiguous (in matters of whitespace), it remains to complete the formal specification of the concrete syntax of JSON with a suitable disambiguation, which we plan to do soon.