{"entities":{"Q4329634":{"pageid":6359235,"ns":120,"title":"Item:Q4329634","lastrevid":47779111,"modified":"2026-01-02T16:22:33Z","type":"item","id":"Q4329634","labels":{"en":{"language":"en","value":"Hoare logic for Java in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1736469"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$43AE0B24-FB14-4294-A195-10B37DB1E4A5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cada8dcf49e59101a479472c288237b917fa2d74","datavalue":{"value":{"text":"Hoare logic for Java in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4329634$8CFFF477-E90A-4353-9DF5-7220C3B96F76","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ae56d1e05de3b057dfbe635252e507e9e39c07ca","datavalue":{"value":"0997.68019","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4329634$61FEBFCA-0EEE-4624-8AC0-8E0DF8067472","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"922ae95e156193bf43196b5e76a08bd2cb8e81fc","datavalue":{"value":{"entity-type":"item","numeric-id":2752049,"id":"Q2752049"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$A30365E8-E309-45FA-816F-651915534C6F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e33c246ddda0f045756f52520d48aca3ce4f9040","datavalue":{"value":{"entity-type":"item","numeric-id":2744780,"id":"Q2744780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$A404E6D8-96B4-47FE-B5CF-A4AF25CAB566","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"8806347b90313b3cbd7ad1edb5b793d4961d7274","datavalue":{"value":{"time":"+2002-11-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4329634$194472FC-E412-49C1-9B70-2EB28983337F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4329634$7E4B01AB-F6F8-415A-ABE7-BBDE4C5817AB","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"eb06534cf456ad55bce4a65264554d6ee84d7d0e","datavalue":{"value":"1736469","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4329634$7B956C5A-0C3E-4742-B9B3-B844DFCC0E79","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d1198f0bbb667512be01aab44ec818144a2be4d8","datavalue":{"value":"Hoare-style calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q4329634$1CE1AF52-63BE-49D6-9B82-56362443C113","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e99c9cb22c11fc5102e4fd7ac02c6495af6cb5bf","datavalue":{"value":"Java Card","type":"string"},"datatype":"string"},"type":"statement","id":"Q4329634$0B887CE0-6FC6-4C80-9AF2-FDB20835C6F1","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$53E9165D-7C27-482C-B744-AE997E981879","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"beb205139d0971fca32ffa61e5b55aaac31a7181","datavalue":{"value":{"entity-type":"item","numeric-id":16768,"id":"Q16768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$445468D7-4244-4E7D-9E83-D829FF88E4A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$33F8BB57-1CDC-4F9B-9F1C-D64188B9B82B","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$A1871FF2-B5EE-4F76-88BA-D3ABEFAFBCC9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fe89da64932247c937489bfcc8fb4e958200c376","datavalue":{"value":"https://doi.org/10.1002/cpe.598","type":"string"},"datatype":"url"},"type":"statement","id":"Q4329634$304F171A-16CD-4991-A229-D2A6FB2E2C31","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"80ee6618ed1470626ede4bb72c54245748965a01","datavalue":{"value":"W1987693120","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4329634$2735E47F-691F-4BF1-AFBF-1BB2F97B2001","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"472cf19de10139786f8a962564dd8595fa33649b","datavalue":{"value":{"entity-type":"item","numeric-id":3122694,"id":"Q3122694"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$9B1C1005-6DD2-450F-8B2B-4D4FCA138E07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0a9134c58e54d930921f3bed1c10f8c24262f2dd","datavalue":{"value":{"entity-type":"item","numeric-id":4230924,"id":"Q4230924"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$D39BCD3F-F395-468C-A922-471577598D7A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8275278c932565b6b1f07c9efa2015518a0375b7","datavalue":{"value":{"entity-type":"item","numeric-id":2754049,"id":"Q2754049"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$AF75EEFA-DDF7-499D-B3B8-76CB4A898DCA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$E6062E55-C761-4DE9-B2D7-8965CFC75F07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b3bc80122c3248b7370a66f915205122d19550f7","datavalue":{"value":{"entity-type":"item","numeric-id":3925144,"id":"Q3925144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$424B5889-B04E-4E7F-B203-E4738A05A08F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$FFD6B2FF-8820-48D6-83F1-808B9EC35530","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ca7e027091589776f78a6d7ad8457e805c17b28","datavalue":{"value":{"entity-type":"item","numeric-id":5777498,"id":"Q5777498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$0776F4B1-B634-4112-917A-845FF0ED8362","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cc8abb92210655a5bd4143cbbadd6eadb52d635","datavalue":{"value":{"entity-type":"item","numeric-id":1801222,"id":"Q1801222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$C288E222-24E9-4576-BB6E-B79093AA689F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$EA0BFE0B-5536-47E5-B06C-F83119CD0436","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d036e5c22d0346ebd8afe2f0065acf9457584fcb","datavalue":{"value":{"entity-type":"item","numeric-id":1566861,"id":"Q1566861"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$D135CF51-18B0-4CAD-B82A-1E84EDAB928A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2c71c26bf7e075dc23cee40b3135f1af13e67a2","datavalue":{"value":{"entity-type":"item","numeric-id":4151703,"id":"Q4151703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$19DDAFE3-51CC-4D9C-A2FF-FE35E798C7B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"689f6b7f9854c12a4cddd7dba59ed43395c8aca7","datavalue":{"value":{"entity-type":"item","numeric-id":1225451,"id":"Q1225451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$1C36F41B-E170-40F6-AC03-376B6BCA22B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c324aa1e4a2f079502797d72067f2c4a5406a497","datavalue":{"value":{"entity-type":"item","numeric-id":3694663,"id":"Q3694663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$D3A49B56-ED9A-4BB9-84B4-BB0F4701358D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa612727e182e3a3dac3e43d5ef047f71f914e20","datavalue":{"value":{"entity-type":"item","numeric-id":2744196,"id":"Q2744196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4329634$6DE4C1FE-C733-4BC9-8855-093CE439406E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"df93c031ceb6c360da04dcc8c66be3bfd87c8850","datavalue":{"value":"10.1002/CPE.598","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4329634$CECBF2B9-3955-4E12-BA66-8CA28423FB21","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8fd5c2832aabbf4b304824c9b3020a0ed9253b4e","datavalue":{"value":{"entity-type":"item","numeric-id":4823141,"id":"Q4823141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3ae0829b3d33101f05cbb7027848b3da8fd6156c","datavalue":{"value":{"amount":"+0.843045711517334","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4329634$4A572735-C366-449F-98A6-18C7DE19216F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"25cda0e867a57a75bd59601979465a0f0bcb93f5","datavalue":{"value":{"entity-type":"item","numeric-id":4808824,"id":"Q4808824"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0ecaf35d079dd669fd0990f04772ad260571808f","datavalue":{"value":{"amount":"+0.8267565965652466","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4329634$EB38A22F-5E51-49CA-8320-025249DAAF53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fa65c7f32f6ba0869650b0738f3e526afcb5338b","datavalue":{"value":{"entity-type":"item","numeric-id":5902541,"id":"Q5902541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4a60c9c22317570f2e1b58527c871ce8520ee739","datavalue":{"value":{"amount":"+0.7919479608535767","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4329634$CBEEDD39-7EC6-4B45-9C65-AC2A82D2A193","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc8c5a073b0d56fd44a79f48ec4fa897b67d4803","datavalue":{"value":{"entity-type":"item","numeric-id":5313002,"id":"Q5313002"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"92f952322cdd2da62a95ede060eefda2021fbdbe","datavalue":{"value":{"amount":"+0.7842042446136475","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4329634$BD310A95-2CE0-473E-8E07-3AFAF3B9E5F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2b6aaebf68c59600c5656aefd5570e3997509162","datavalue":{"value":{"entity-type":"item","numeric-id":2026792,"id":"Q2026792"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"330ebde5c60082f9b583ebed525279d5ef1e6129","datavalue":{"value":{"amount":"+0.7828131914138794","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4329634$4F41428B-5D01-4944-A5AA-0DA30EBA163E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4329634","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4329634"}}}}}