{"entities":{"Q789887":{"pageid":791735,"ns":120,"title":"Item:Q789887","lastrevid":64360707,"modified":"2026-04-11T19:20:05Z","type":"item","id":"Q789887","labels":{"en":{"language":"en","value":"Proving program inclusion using Hoare's logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3846837"}},"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":"Q789887$814F3CA3-17C5-445C-8FD9-62D42FD9D539","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d67a8064968d66e72c48834478ca3bab7f26e355","datavalue":{"value":{"text":"Proving program inclusion using Hoare's logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q789887$DA9A33DC-936B-482B-B71B-C84477DE7639","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"00f5677104d7270cd2a3c8afa137d31f0a50f1ec","datavalue":{"value":"0533.68011","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q789887$5D108E4F-4D01-4B04-B10B-7EF0A3008A4C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3e6c6e81599d6a7b6bab693c90d8099563c135b7","datavalue":{"value":"10.1016/0304-3975(84)90065-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q789887$037A9E1E-7D85-4EC2-9087-114E122C0456","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$7CD71370-ED8E-4530-8C7A-30695AB360A2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2ee0f220147ae8bc749a64db56839865dbc4f127","datavalue":{"value":{"time":"+1984-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q789887$CAF843BA-B563-44D7-9240-28A7263E3946","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9c7d365318d0bad02ba0d04b6d73008eb6304e0a","datavalue":{"value":"https://ir.cwi.nl/pub/1833","type":"string"},"datatype":"url"},"type":"statement","id":"Q789887$D26BA12F-0144-4D69-ADE8-EC1B6D4EAEC5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q789887$EEF16373-5F1A-46E2-BA3C-54A9D69A98D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"14cf74de25853c940589b125137b792dfb2d092b","datavalue":{"value":"68P05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q789887$0351E983-2D3D-4A57-8B5F-014653B8EE2D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"21a9f7697d33d33d45dddc0f3b886f16239fb7d7","datavalue":{"value":"3846837","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q789887$0070A8C4-E805-417D-AAC1-5D47BCC0D3E1","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"168efd5b5ea5201f07981f3c97023441918073bd","datavalue":{"value":"data type specification","type":"string"},"datatype":"string"},"type":"statement","id":"Q789887$0F33C5BD-4E9B-4DD6-9753-64EE680A75ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d454932b423821d66b02d6797562c28eb464def4","datavalue":{"value":"conservative refinement","type":"string"},"datatype":"string"},"type":"statement","id":"Q789887$5AABEECE-03E5-48C9-874D-278E5620859B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4dac5de8e537c71cd90df166682399621b2f7fbf","datavalue":{"value":"program equivalence","type":"string"},"datatype":"string"},"type":"statement","id":"Q789887$17879F9E-C555-403F-92BD-EB6417EFF18D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e8c0c4f3af716cb0f3ccf15773255c3f017efbbe","datavalue":{"value":"prototype proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q789887$FDD3C31B-E117-48DD-9AB0-03A876D46B7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2390ef377ab756efa9f2686dcaa637fdda91c839","datavalue":{"value":"logical completion","type":"string"},"datatype":"string"},"type":"statement","id":"Q789887$BD815534-9527-4B12-B565-A2B55DB59639","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a2b746efc66121bc1fb497da4ab39b83b5cd2f4c","datavalue":{"value":"program correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q789887$C0BC4A31-ECEB-4F47-86A7-A50388BA1E4F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"78ed6c5ce1e65f91c49ded91114a6800dd345a5d","datavalue":{"value":{"entity-type":"item","numeric-id":190306,"id":"Q190306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$FF095E8D-D95C-4BCF-88CC-8511846AE55B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8a6741b206af4ec153c5c61303c48d28d7dd1242","datavalue":{"value":{"entity-type":"item","numeric-id":549184,"id":"Q549184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$31ADE376-3062-4330-BD10-6E6F15F960D8","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":"Q789887$91DA0304-8534-44AC-93EE-07EB5F279E7A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d770bc35fdb2ffb22c6769974de5bb79fa3f9ec2","datavalue":{"value":"W2150726636","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q789887$4BA555AD-5098-4EE1-B3E2-4534422D78B1","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"78296e26b3ae6866aa6457e77aa0a789c0969d64","datavalue":{"value":{"entity-type":"item","numeric-id":3862382,"id":"Q3862382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$71C02DC6-53FF-4AA9-8702-5ECC3B670548","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7469a14c6b3d5214a08da9b6d9960375ad8bda98","datavalue":{"value":{"entity-type":"item","numeric-id":3898009,"id":"Q3898009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$C2C6BD57-6D4E-4EF1-B0C9-7E4A37636102","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0fef7db710aa93e9f87a9f7584dba9019913b4b5","datavalue":{"value":{"entity-type":"item","numeric-id":5181349,"id":"Q5181349"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$9CCBF147-DA5B-4479-8D42-365F6420C143","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fb12b188658ef9d46086882edec316113d94d7af","datavalue":{"value":{"entity-type":"item","numeric-id":3899466,"id":"Q3899466"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$33A7A5B3-594D-48D6-A411-3C99832D40D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4fc01beee0576bea6ea525779afa0e96e85c3165","datavalue":{"value":{"entity-type":"item","numeric-id":1158948,"id":"Q1158948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$FAAD8E0D-D158-4029-99C6-A0646F2590B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"204a60a0dd6db59a13ec2fe13a81900fc611c22f","datavalue":{"value":{"entity-type":"item","numeric-id":3929010,"id":"Q3929010"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$584A12ED-28A3-4B92-A459-3940179345BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c23a54cf5c2c32f027cfca2700657a849c9c7aec","datavalue":{"value":{"entity-type":"item","numeric-id":800082,"id":"Q800082"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$45EB3C19-68EC-443C-8FA4-C23B470D1442","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"271435b73e7162645c02aeae8f7365e9fe6491de","datavalue":{"value":{"entity-type":"item","numeric-id":4741695,"id":"Q4741695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$17494542-56AA-46D7-8303-B05F135E9F1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e57c1ff39f8d8b1f50daf676885aeffc53a7754","datavalue":{"value":{"entity-type":"item","numeric-id":1170877,"id":"Q1170877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$FF1539B7-2B1E-4991-ACEF-5EF78FDFFA64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4379ac82957e0d469358f8f6b45d2e327b196b52","datavalue":{"value":{"entity-type":"item","numeric-id":794426,"id":"Q794426"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$E82432B3-C1F6-438F-BFEA-1E0478967001","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3be99e1f896a6838dd0f91ded8130808d4f1089","datavalue":{"value":{"entity-type":"item","numeric-id":4052072,"id":"Q4052072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$A9ACFF0C-1165-4FFD-8926-A159CAD53282","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f067c1b808884e93605e1af2dbca3dd82129f7ed","datavalue":{"value":{"entity-type":"item","numeric-id":4170195,"id":"Q4170195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$5A754A0D-E2C8-44B5-B74A-05544E57C178","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":"Q789887$4EE24122-04E7-494A-8DB0-95D79D01D737","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ca4f823ca2e82e86e612699cdb65f38c133999d","datavalue":{"value":{"entity-type":"item","numeric-id":4052071,"id":"Q4052071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$10E9B13F-8F16-439E-A60B-D7A6766E5B9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb3ca9fc3aae0e682a4fb157c408b25328a8cbcf","datavalue":{"value":{"entity-type":"item","numeric-id":2561836,"id":"Q2561836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$D17B45CF-0364-4B3A-81A6-F4407EF8A7FB","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":"Q789887$DA71AC44-8A41-4B20-A6C1-77F5ECE0CBF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1950b2f7ea4f55b053fe30cb31fae70c4ce589d","datavalue":{"value":{"entity-type":"item","numeric-id":3848975,"id":"Q3848975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$03D6721C-5DAA-4444-A40E-F62FCA3EC8D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"914ef8719678eb4ee59028ba65b4741c8aa1bc8e","datavalue":{"value":{"entity-type":"item","numeric-id":4124327,"id":"Q4124327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$4FBB8E12-D77B-4D7F-83A4-9E9E0165DDC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9378587a1115a0250a2395ebd434016b1bcd6dd","datavalue":{"value":{"entity-type":"item","numeric-id":4124795,"id":"Q4124795"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$5AE3B19D-12FB-4E31-B140-3A35EA6CF97C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9635365b0780328d7ae22bc69b462e7144999d03","datavalue":{"value":{"entity-type":"item","numeric-id":5573961,"id":"Q5573961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$A36B1728-E36F-40A3-9B9F-5849DFE49CEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"473a4395cf9d648485e8d538f74096f90afb9dfe","datavalue":{"value":{"entity-type":"item","numeric-id":1138902,"id":"Q1138902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$A3EECF6B-F055-49B8-85FA-787A4A68BBDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3f40bcaa8d311e4db512eab174f3dec9cd00f54c","datavalue":{"value":{"entity-type":"item","numeric-id":5537599,"id":"Q5537599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$3599A4F8-23A0-464F-BCA6-B7C4A9D74BAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"377324767631186c74643cd4927092bc831167c8","datavalue":{"value":{"entity-type":"item","numeric-id":4139636,"id":"Q4139636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q789887$D1D4F5A0-E2C2-4E1E-A2AD-25893573E172","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"920a9b4736e3dc9bdd0f1f07e717de567cd54fde","datavalue":{"value":{"entity-type":"item","numeric-id":3678649,"id":"Q3678649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"66e43a5fafd0350bd02027f5418065e6be019e4d","datavalue":{"value":{"amount":"+0.7575300931930542","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":"Q789887$1B674915-C7D0-4718-9C2E-E9368824152F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e2201ceba745f8f4bc88d73a6cab694ed61248d5","datavalue":{"value":{"entity-type":"item","numeric-id":794426,"id":"Q794426"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b3b9bdde1ff601c687b3e8e1ca5c1ec8bec712c","datavalue":{"value":{"amount":"+0.7520374059677124","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":"Q789887$C4992A93-408B-407A-B64E-C8CE646748C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ef5e699799c57d1a4581c931d902b74e8d7efb95","datavalue":{"value":{"entity-type":"item","numeric-id":672320,"id":"Q672320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f038f2cb8120fd98725a97b9347fdc4436628ddf","datavalue":{"value":{"amount":"+0.7500410676002502","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":"Q789887$1C11EE98-208B-4494-88E3-9B1498ADEBEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6eb935c4e813b5a39add7d74a332bab4384bf192","datavalue":{"value":{"entity-type":"item","numeric-id":685395,"id":"Q685395"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3a6ec1515512119bd0325c1fd11a3245fd2643b0","datavalue":{"value":{"amount":"+0.7457635998725891","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":"Q789887$D65961D0-0759-4ECE-93E0-1FC05CC38D2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7ea95e49f05526edb7368d843c6ed27a9c17b632","datavalue":{"value":{"entity-type":"item","numeric-id":4923522,"id":"Q4923522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3a6ec1515512119bd0325c1fd11a3245fd2643b0","datavalue":{"value":{"amount":"+0.7457635998725891","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":"Q789887$FA15C92A-3F09-4C23-A7D2-F2D23C4DE228","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proving program inclusion using Hoare's logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Proving_program_inclusion_using_Hoare%27s_logic"}}}}}