{"entities":{"Q1322851":{"pageid":1333601,"ns":120,"title":"Item:Q1322851","lastrevid":67173315,"modified":"2026-04-12T15:47:08Z","type":"item","id":"Q1322851","labels":{"en":{"language":"en","value":"On the mechanical derivation of loop invariants"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 566071"}},"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":"Q1322851$8365D14A-0301-413B-9E29-9746A3BDF22C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cbfceb6014e7efb7cf4dbdccbbb2344035137263","datavalue":{"value":{"text":"On the mechanical derivation of loop invariants","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1322851$A5C00852-7845-4889-84D2-A2D0EF15D012","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0d26ead760a7d99e3cb2de428967e556a007eaf6","datavalue":{"value":"0804.68129","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1322851$F1897A80-3472-434A-819E-8BCB19A76B6F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"210c7af791486a20a259be181bd03ee9b59bea13","datavalue":{"value":"10.1016/S0747-7171(06)80010-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1322851$D408036F-F07D-4E98-8407-466F48CB1E3B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a5a0455bdbd3c6bb9633e92150aff79390c6a3ea","datavalue":{"value":{"entity-type":"item","numeric-id":1322850,"id":"Q1322850"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322851$9FB5BEED-0220-4F85-BDCA-1A23D4AEE0A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"34f99c9947f4d98af9da609b6496b55645bbe075","datavalue":{"value":{"entity-type":"item","numeric-id":1238600,"id":"Q1238600"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322851$129D0799-B1C8-440D-939C-799B14EFC084","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ea72303f92787da89554ee5fa15621068821a762","datavalue":{"value":{"entity-type":"item","numeric-id":99061,"id":"Q99061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322851$46D867E2-24C8-4FC8-A5FF-394BB4502A99","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f0b9742ce47347ab40f936186bf0b8d8c03fdc54","datavalue":{"value":{"time":"+1995-01-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1322851$5E051B50-DBED-4687-AF4B-AD965BD96FBD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1322851$F7DD93AA-E536-406B-B873-CD568AE7260C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1322851$AFFBA26D-1EFA-45FF-9CFB-5D62C8BE6651","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1322851$F6EE76B8-59DF-41D7-826C-2D4B85E709D6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1e92cb6800fcc63ffd1f2b716b6061e3fbe7b407","datavalue":{"value":"566071","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1322851$E9A8FDAE-B5E8-43D0-9A5D-70A1557DB7A7","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"767caa3fec8ab19292904d029121096f17ce8d53","datavalue":{"value":"flowchart program","type":"string"},"datatype":"string"},"type":"statement","id":"Q1322851$A6656E20-B99A-452B-94B5-FE7F39B8574C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5c12c3aa988768f7c70e3e2a36374b0b57fe3df1","datavalue":{"value":"iterative algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q1322851$A314588E-45D2-4381-AAF0-4633822BEDEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5c6b234052d577bbfc0605fdbf112f40bb1c4228","datavalue":{"value":"loop invariants","type":"string"},"datatype":"string"},"type":"statement","id":"Q1322851$44497AC2-A677-41EF-BC2F-901268AFBEAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4f07bce2247891a2f210361f1727683ab7836f4a","datavalue":{"value":"partial correctness of programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1322851$1C3326A3-4FF0-47F8-A425-8DA36D15130C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1322851$C85BFA35-F401-4734-AA41-8ACCAEF5BB0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8a91686b786ccf10b18d57a44c0fa4f9d974b18c","datavalue":{"value":"unskolemization","type":"string"},"datatype":"string"},"type":"statement","id":"Q1322851$3B92811A-1538-478E-97FF-522AD5EFC540","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":"Q1322851$9111142A-8D28-47EE-B49A-741B925BDD1A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a4735154d50c08d584a8e28202802fa9d661654","datavalue":{"value":{"entity-type":"item","numeric-id":5679729,"id":"Q5679729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322851$B2BD878D-7CBB-4704-8FA4-DFF0B3B45E3F","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":"Q1322851$94BB9B5A-353A-48BA-A7D3-B178EF890270","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"905bced2f4ed2fada959527f35930716f00e84f3","datavalue":{"value":{"entity-type":"item","numeric-id":5677070,"id":"Q5677070"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322851$AE98C660-A5D4-4F8B-9026-2A31A486E950","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"715a321cfec84df9fa9f2ee50c176f70cf073ba7","datavalue":{"value":{"entity-type":"item","numeric-id":1059063,"id":"Q1059063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322851$407212D1-404A-4A45-A90E-EF3DC1117904","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2286eb334c2f9f8a0f652d8c77c5da98301799fc","datavalue":{"value":{"entity-type":"item","numeric-id":3334052,"id":"Q3334052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322851$5736EFA5-1E97-43AA-A317-AA478F261F76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6130a72bad290e99b4d30823cf592f64ef05b4a8","datavalue":{"value":{"entity-type":"item","numeric-id":5584402,"id":"Q5584402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322851$BE49D56D-730E-4EF2-9403-A10E4CA101AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"924ff67e0ddb99ec0fa6c2e268cb0f96cfabe058","datavalue":{"value":{"entity-type":"item","numeric-id":3334054,"id":"Q3334054"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322851$71AFAABA-A01C-446D-A2B4-9D7ADB77A1CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e47b8c90d45ee285590b1a168a8503851fe5b134","datavalue":{"value":{"entity-type":"item","numeric-id":3925859,"id":"Q3925859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322851$868D0A37-136A-4837-8D08-87DC63F5BE7A","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":"Q1322851$4477A44E-0E44-497F-901C-E216106947A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2bc7c80135ed65b38d7fef7c0e832d27cd87588f","datavalue":{"value":{"entity-type":"item","numeric-id":3995530,"id":"Q3995530"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322851$C81DC50A-C6DB-46A1-AF7D-3AB6D2EC45BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1aa9e8bb4ef37ec285d6c238c3f5aa5ed5c9a38","datavalue":{"value":{"entity-type":"item","numeric-id":4139711,"id":"Q4139711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322851$95309BF6-59CD-4AEA-966C-0E8DCAB0FB99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6aeaa612994b5e9a2092feccaf55cd8c93f37bbc","datavalue":{"value":{"entity-type":"item","numeric-id":920968,"id":"Q920968"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322851$F1F0A2EF-12A8-432C-9C40-3600A79A0A8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322851$7047E9F3-FA07-4D08-89E1-0A8176E6519B","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":"Q1322851$0D6A5617-D942-4E6A-9252-943EB06EE825","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"432bb74448aab66737929b46e8d9d49596ec6125","datavalue":{"value":"https://doi.org/10.1016/s0747-7171(06)80010-6","type":"string"},"datatype":"url"},"type":"statement","id":"Q1322851$83AD77B0-E32B-40C0-8098-C8D75D29A037","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ace61873c842c09dc41022e2801b1d369c970bb1","datavalue":{"value":"W2093349003","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1322851$B7E119C4-BB93-4372-8AE3-1A2E0F6493D2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f464b64c5ce744bcc9e044bb866ec7efefd38317","datavalue":{"value":{"entity-type":"item","numeric-id":604381,"id":"Q604381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2d925133d3646a6819cd1a8cab24bfc31acb5101","datavalue":{"value":{"amount":"+0.8012889623641968","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":"Q1322851$6C5C9309-EA15-4D75-AD93-A0E8C19CC6CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ecf08f9e6eae6c33e54be636f8491d559294d6d6","datavalue":{"value":{"entity-type":"item","numeric-id":3004678,"id":"Q3004678"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c7efb7be507104abf78bc9ad2d3eb6da578c6c6c","datavalue":{"value":{"amount":"+0.7802575826644897","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":"Q1322851$F1FAAE67-F326-407B-B1A3-6035AD14BA22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"725bb17ca3657881f0a98dc3d779187baeabced2","datavalue":{"value":{"entity-type":"item","numeric-id":3656883,"id":"Q3656883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa4ce73953a3c415657febcbd0ace3c3fbdc1dd6","datavalue":{"value":{"amount":"+0.779370129108429","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":"Q1322851$FE222E85-B963-45B5-BE29-1533F9255AD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e36f3694c49ffa7483df2a818342d806f5dea076","datavalue":{"value":{"entity-type":"item","numeric-id":5740643,"id":"Q5740643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b24c6a0305b7b56a450b692592cc0d4e593a4648","datavalue":{"value":{"amount":"+0.7749488949775696","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":"Q1322851$FB9D6489-BB56-47A8-9C5C-184DB8CDCE90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a6e4251c7d7c8287cb43fb5e0e28c5f0d5fdbdab","datavalue":{"value":{"entity-type":"item","numeric-id":1065537,"id":"Q1065537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7d8ca178234bda20bc61eb71bcfbb80c7da41c01","datavalue":{"value":{"amount":"+0.7689440250396729","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":"Q1322851$D490C771-2B3D-4FA5-A4AE-1DDFBC840211","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On the mechanical derivation of loop invariants","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/On_the_mechanical_derivation_of_loop_invariants"}}}}}