JSONUtil

JSON parser/printer for VDM-SL

CAUTION : JSONUtil does NOT distinguish “” and [] because neither does VDM-SL.

JSON <-> VDM mappings

JSON = seq of char;
STRING = seq of char;
ARRAY = seq of VALUE;
OBJECT = map STRING to VALUE;
NUMBER = real;
BOOL = bool;
VALUE = [ STRING | ARRAY | OBJECT | NUMBER | BOOL ];

exports the following functions

parseJSON : JSON -> bool * VALUE;

parses the given JSON string into a VDM value. This function permits extra data after a valid JSON portion.

parseJSON("[1, true, \"string\", {\"key\":\"value\"}]")
==> mk_(true, [1, true, "string", {"key" |-> "value"}])
parseJSON("[1, true, \"string\", {\"key\":\"value\"}] EXTRA") 
==> mk_(true, [1, true, "string", {"key" |-> "value"}])

strictParseJSON : JSON -> bool * VALUE;

parses the given JSON string into a VDM value. This function does NOT permit extra data after a valid JSON portion.

strictParseJSON("[1, true, \"string\", {\"key\":\"value\"}]")
==> mk_(true, [1, true, "string", {"key" |-> "value"}])
strictParseJSON("[1, true, \"string\", {\"key\":\"value\"}] EXTRA")
==> mk_(false, nil)

printJSON : VALUE -> JSON;

prints the VALUE values into JSON format.

printJSON([1, true, "string", {"key" |-> "value"}])
==> "[1, true, \"string\", {\"key\":\"value\"}]"