JSON and Sockets: Difference between revisions

Revision as of 07:15, 28 March 2025

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)

Revision as of 07:13, 28 March 2025 view source Michael Leuschel (talk \| contribs) Bureaucrats, Administrators 3,330 edits No edit summary ← Older edit		Revision as of 07:15, 28 March 2025 view source Michael Leuschel (talk \| contribs) Bureaucrats, Administrators 3,330 edits No edit summary Newer edit →
Line 3:		Line 3:
	* <tt>LibraryJSON.def</tt> and <tt>LibraryJSON.mch</tt> providing the functions <tt>READ_JSON</tt>, <tt>READ_JSON_FROM_STRING</tt>, <tt>WRITE_JSON</tt>, <tt>WRITE_JSON_TO_STRING</tt> and the freetype <tt>JsonValue</tt> to read and write JSON data.		* <tt>LibraryJSON.def</tt> and <tt>LibraryJSON.mch</tt> providing the functions <tt>READ_JSON</tt>, <tt>READ_JSON_FROM_STRING</tt>, <tt>WRITE_JSON</tt>, <tt>WRITE_JSON_TO_STRING</tt> and the freetype <tt>JsonValue</tt> to read and write JSON data.

	* <tt>LibraryZMQ_RPC.def</tt> and <tt>LibraryZMQ_RPC~~.mch</tt>: providing access to a JSON communication library either over regular sockets or ZMQ sockets~~.mch</tt>: providing access to a JSON RPC (Remote Procedure Call) library either over regular sockets or ZMQ sockets~~. More information is available on [[JSON and Sockets]]~~.		* <tt>LibraryZMQ_RPC.def</tt> and <tt>LibraryZMQ_RPC.mch</tt>: providing access to a JSON RPC (Remote Procedure Call) library either over regular sockets or ZMQ sockets.