Working with JSON-Formatted Data in Isabelle
JSON (JavaScript Object Notation) is common format for exchanging data. Thus, sometimes it would be handy to be able to “import” JSON-formatted data into Isabelle/HOL, e.g., as part of a datatype package (implemented in Isabelle/ML) for using the data as part of a system verification (in Isabelle/HOL).
Using our AFP entry “Nano JSON” [1] this is now easy. It provides both import and export of JSON-formatted data into Isabelle - both on the level of Isabelle/ML and Isabelle/HOL. Thus, it allows users of Isabelle/HOL to work with JSON-formatted data in Isabelle without needing to implement import or export functionalities in ML. At the same time, user that want to implement their own datatype package can use the Isabelle/ML API provided by AFP entry “Nano JSON”.
For example, assuming a simple JSON encoded data like
{
"menu": {
"id": "file",
"value": "File",
"popup": {
"menuitem": [
{"value": "New", "onclick": "CreateNewDoc()"},
{"value": "Open", "onclick": "OpenDoc()"},
{"value": "Close", "onclick": "CloseDoc()"}
]
}
},
"flag":true,
"number":42
}
stored in a file example.json
, you can now import this data into
Isabelle
JSON_file "example.json" defining example
and use it in a formal context, such as
lemma ‹([STR ''onclick''], STRING STR ''CreateNewDoc()'') ∈ set(nj_filter (STR ''onclick'') example_literal_literal)›
by(normalization)
Alternative ways of importing JSON
For short JSON-snippets, you can use an antiquotation:
lemma ‹y == JSON ‹{"name": true}› ›
oops
Moreover, for you can also use a new Isar command that allows for inlining JSON into Isabelle theories:
JSON ‹
{
"menu": {
"id": "file",
"value": "File",
"popup": {
"menuitem": [
{"value": "New", "onclick": "CreateNewDoc()"},
{"value": "Open", "onclick": "OpenDoc()"},
{"value": "Close", "onclick": "CloseDoc()"}
]
}
},
"flag":true,
"number":42
}
› defining example04
Exporting JSON
Exporting JSON is easy, assuming that the data has already been converted the HOL-representation of JSON provided:
JSON_export example file example