{"entities":{"Q7361045":{"pageid":31518674,"ns":120,"title":"Item:Q7361045","lastrevid":105362498,"modified":"2026-10-07T13:34:13Z","type":"item","id":"Q7361045","labels":{"en":{"language":"en","value":"pGCL for Isabelle"}},"descriptions":{"en":{"language":"en","value":"AFP entry pGCL"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6c8b5118e58b5d64943d751d5eb04e5924f3d52a","datavalue":{"value":"https://isa-afp.org/entries/pGCL.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361045$11700944-AB24-4D44-8910-ED3DC0EC664A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"699e379f808064d2978158ea55994236cc66fbee","datavalue":{"value":{"time":"+2014-07-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361045$1BB69794-F006-418F-A43F-392D41AD59C2","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"937e195639854856e0dfb38f63b2f06d2d661182","datavalue":{"value":"David Cock","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361045$FFE717B9-AF44-4C55-8148-A59FD245FE28","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cc914509843fe0339f9cfc13fc54cc9cfe31a297","datavalue":{"value":{"text":"pGCL for Isabelle","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361045$56B0046C-5785-462F-AB62-F7CF81962AA5","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b5b281f58180d6cbb463f8dca4ef27dfd0d24023","datavalue":{"value":"pGCL is both a programming language and a specification language that incorporates both probabilistic and nondeterministic choice, in a unified manner. Program verification is by refinement or annotation (or both), using either Hoare triples, or weakest-precondition entailment, in the style of GCL. This package provides both a shallow embedding of the language primitives, and an annotation and refinement framework. The generated document includes a brief tutorial.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361045$C04F10A6-3453-455B-A7E8-2789151FF9E3","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a2dc34bc3d22c65ca26ace9ca84fe6e53af6e81c","datavalue":{"value":{"entity-type":"item","numeric-id":5327352,"id":"Q5327352"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361045$0CBBB646-EDA0-4440-A5AD-B0A579ACB3A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1265d63b4599a3fae507d9b15943296bbefa977b","datavalue":{"value":{"entity-type":"item","numeric-id":4066568,"id":"Q4066568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361045$0FDAF566-9A07-44F2-A4B4-E68754336432","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f81309e87becee3cda8d7174d2d8b5b31baaaeac","datavalue":{"value":{"entity-type":"item","numeric-id":2576950,"id":"Q2576950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361045$B1148B3A-D26F-472C-9A3D-36B2CCADA668","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361045$D47E8C18-3B08-44FD-B8A7-52BDCA498E4C","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"9beb5f7be6b27e22c4af581585b828086bbf7950","datavalue":{"value":{"entity-type":"item","numeric-id":7360796,"id":"Q7360796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361045$AACBDF4A-3C4D-47E1-9440-154B10B4EE05","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361045$9BE4AEAC-834B-4D98-BE32-26976C56283F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"PGCL for Isabelle","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/PGCL_for_Isabelle"}}}}}