JSON and Sockets

ProB contains external functions to read and write JSON data and to communicate via sockets using JSON:

• LibraryJSON.def and LibraryJSON.mch providing the functions READ_JSON, READ_JSON_FROM_STRING, WRITE_JSON, WRITE_JSON_TO_STRING and the freetype JsonValue to read and write JSON data.

• LibraryZMQ_RPC.def and LibraryZMQ_RPC.mch: providing access to a JSON RPC (Remote Procedure Call) library either over regular sockets or ZMQ sockets.

LibraryJSON.mch defines a FREETYPE to represent JSON data in a type-safe way:

  JsonValue = JsonNull,
              JsonBoolean(BOOL),
              JsonNumber(FLOAT),
              JsonString(STRING),
              JsonArray(seq(JsonValue)),
              JsonObject(STRING +-> JsonValue)

Free Types are inductive data types. They are not standard B, but stem from Z and Rodin's theory plug-in.

LibraryZMQ_RPC.mch defines a FREETYPE to represent RPC in a type-safe way:

 RpcResult = RpcSuccess(JsonValue), RpcError(STRING)

We have used this library to control Crazyflie drones via ProB: